A Quantum SMT Solver for Bit-Vector Theory

Shang-Wei LinSi-Han ChenTzu-Fan WangYean-Ru Chen

Mar 2023

摘要

Given a formula $F$ of satisfiability modulo theory (SMT), the classical SMTsolver tries to (1) abstract $F$ as a Boolean formula $F_B$, (2) find a Booleansolution to $F_B$, and (3) check whether the Boolean solution is consistentwith the theory. Steps~{(2)} and (3) may need to be performed back and forthuntil a consistent solution is found. In this work, we develop a quantum SMTsolver for the bit-vector theory. With the characteristic of superposition inquantum system, our solver is able to consider all the inputs simultaneouslyand check their consistency between Boolean and the theory domains in one shot.

展开全部

图表提取

论文十问

参考文献

被引用

提问与回答

暂无人提供速读十问回答

被引用

笔记

问答

领域