Quantangle-SAT: A Quantum SAT Solver Based on Entanglement and Equivalence Checking

TL;DR

This paper introduces Quantangle-SAT, a quantum SAT solver leveraging entanglement and equivalence checking, which does not require prior solution count knowledge and offers efficient expected performance.

Contribution

It presents a novel quantum SAT solving method that avoids the limitations of Grover-based approaches by eliminating the need for solution count estimation.

Findings

Expected time complexity is constant O(1) over random Boolean functions.

Experimental results support the theoretical efficiency claim.

The method is more computationally efficient than quantum counting.

Abstract

Satisfiability (SAT) is a central problem in computer science, and advances in SAT-solving algorithms have a far-reaching impact across many fields. Recent works have proposed quantum SAT solvers based on Grover's algorithm, a quantum search technique. However, Grover-based approaches face a key limitation: they typically require prior knowledge of the number of satisfying assignments of the target Boolean formula. This information is unavailable in most practical settings. Quantum counting can be used to estimate this quantity, but it incurs a computational overhead that is several orders of magnitude higher than Grover search. In this paper, we propose a novel quantum SAT solver based on entanglement and equivalence checking. Our method does not assume prior knowledge of the number of solutions and is computationally more efficient than quantum counting. Although the worst case time complexity is inevitably exponential, we prove that the expected time complexity of our approach is only constant time O(1) over random Boolean functions. Experimental results also support our theoretical claim.