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 (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.

翻译：给定可满足性模理论（SMT）公式$F$，经典SMT求解器尝试：(1) 将$F$抽象为布尔公式$F_B$，(2) 找到$F_B$的一个布尔解，以及(3) 检验该布尔解是否与理论一致。步骤(2)和(3)可能需要反复交替执行，直至找到一致解。在本工作中，我们为位向量理论开发了一种量子SMT求解器。借助量子系统中的叠加特性，我们的求解器能够同时考虑所有输入，并一次性检验它们在布尔域与理论域之间的一致性。