A Quantum SMT Solver for Bit-Vector Theory

Shang-Wei Lin, Si-Han Chen, Tzu-Fan Wang +1

Given a formula $F$ of satisfiability modulo theory (SMT), the classical SMT solver tries to (1) abstract $F$ as a Boolean formula $F_B$, (2) find a Boolean solution to $F_B$, and…