量子科技中心_量科网

布尔可满足性 (SAT) 问题是一个典型的 NP 完全问题，也是通过基于搜索的算法实现量子加速的自然候选对象。在基于 Grover 的量子 SAT 求解器中，主要的计算成本来自于构建评估布尔公式的可逆 oracle，这使得 SAT 编码的选择对于整体量子资源效率至关重要。尽管 SAT 实例通常以合取范式 (CNF) 表达，但这种编码通常会转化为具有显著量子比特开销和高非 Clifford 门复杂度的量子电路。在这项工作中，该团队研究了一种面向量子 SAT 求解的基于异或和之积 (ESOP) 的 CNF (e-CNF) 表示，并分析了其对 oracle 构建的影响。该团队推导了当采用 e-CNF 编码替代标准 CNF 时，基于 Grover 的 SAT 求解器在量子比特需求和 Clifford+$T$ 门数量上的更严格上界。此外，该团队提出了一种从布尔公式到 e-CNF 的可扩展转换方法，并给出了一套将 e-CNF 表示解释为适用于 oracle 实现的可逆量子电路的系统化流程。在代表性 SAT 基准测试上的实验评估表明，与基于 CNF 的 oracle 构建相比，所提出的基于 e-CNF 的方法在量子资源（包括量子比特数、T 门复杂度和电路深度）上实现了显著且一致的缩减。这些结果确立了 e-CNF 作为一种有效的量子感知 SAT 编码，显著提升了基于 oracle 的量子 SAT 求解的实用性。