A Quantum SMT Solver for Bit-Vector Theory
Logic in Computer Science
2023-03-17 v1 Quantum Physics
Abstract
Given a formula of satisfiability modulo theory (SMT), the classical SMT solver tries to (1) abstract as a Boolean formula , (2) find a Boolean solution to , 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.
Cite
@article{arxiv.2303.09353,
title = {A Quantum SMT Solver for Bit-Vector Theory},
author = {Shang-Wei Lin and Si-Han Chen and Tzu-Fan Wang and Yean-Ru Chen},
journal= {arXiv preprint arXiv:2303.09353},
year = {2023}
}