A Quantum SMT Solver for Bit-Vector Theory

Satisfiability modulo theory (SMT), a problem of determining the satisfiability of a first-order formula with respect to a decidable first-order theory, has a wide range of applications because of its powerful ability of problem encoding, including formal verification and optimization workflows in both classical and quantum domains. Given an SMT formula$F$, the classical lazy approach for SMT solving tries to (1) abstract$F$to a Boolean formula$F_{B}$, (2) find a Boolean solution to$F_{B}$, and (3) check whether the Boolean solution is consistent with the theory. If the solution found in the Boolean domain is not consistent with that in the theory domain, the SMT solver needs to perform steps (2) and (3) back and forth until a consistent solution is found between the theory and Boolean domains. This classical approach becomes unscalable when the search space is huge. In this work, we develop the first Grover–based quantum SMT solver to solve formulas on the theory of bit-vectors. With the characteristic of superposition in quantum computing, the proposed SMT solver is able to consider all the possible inputs simultaneously and check their consistency between the theory and Boolean domains in one shot, which brings significant speed-up for SMT solving.