2023/03/16 by Lin, Shang-Wei, Chen, Si-Han, Wang, Tzu-Fan +1
#FOS: Computer and information sciences #FOS: Physical sciences #Logic in Computer Science (cs.LO) #Quantum Physics (quant-ph)
paper · doi:10.48550/arxiv.2303.09353
Given a formula F of satisfiability modulo theory (SMT), the classical SMT solver tries to (1) abstract F as a Boolean formula FB, (2) find a Boolean solution to FB, and (3) check whether the Boolean solution is consistent with the theory. Steps~(2) and (3) may need to be performed back and forth until a consistent solution is found. In this work, we develop a quantum SMT solver for the bit-vector theory. With the characteristic of superposition in quantum system, our solver is able to consider all the inputs simultaneously and check their consistency between Boolean and the theory domains in one shot.