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 解答器试图(1) 抽象地用F$作为布尔值的公式 $F_B$,(2) 寻找布尔值的解决方案 $F_B$,(3) 检查布尔值的解决方案是否与理论一致。在找到一致的解决方案之前,可能需要前后执行步骤<unk> (2)}和(3)。在这项工作中,我们为比特矢量理论开发了量子 SMT 解答器。由于量子系统中的超定位特性,我们的解答器能够同时考虑所有输入,并一次性检查布尔值与理论域的一致性。</s>