A Quantum-Classical Hybrid Algorithm for Solving k-SAT Problems

Boolean Satisfiability Problems (SAT) are used in the programming of systems that have certain criterion that must be met. The complexity of SAT problems increases as the number of literals k, increases. SAT problems are NP complete decision problems, and all SAT algorithms require worst-case exponential time. One of the most effective known classical algorithms for solving k-SAT problems was developed by Uwe Schöning in 1999. While the original algorithm chooses an unsatisfied clause at random and utilizes repetitive bit toggling, a quadratic speed up over Schöning’s algorithm can be achieved by instead using Quantum Amplitude Amplification. The hybrid algorithm is built with IBM Quantum Lab and tools available from Qiskit