We study PRODSAT-QSAT($k$): given rank-one $k$-local projectors, determine whether a quantum $k$-SAT instance admits a satisfying product state. We present a CDCL-style refutation framework that searches a finite partition of each qubit's Bloch sphere while a sound theory solver checks region feasibility using a geometric overapproximation of the projection amplitudes for each constraint. When the theory solver proves that no state in a region can satisfy a constraint, it produces a sound conflict clause that blocks that region; accumulated blocking clauses can yield a global result of product-state unsatisfiability (UN-PRODSAT). We formalise the problem, prove the soundness of the clause-learning rule, and describe a practical algorithm and implementation.

翻译：我们研究PRODSAT-QSAT($k$)：给定秩为1的$k$局域投影算子，判断一个量子$k$-SAT实例是否存在满足条件的乘积态。我们提出一种CDCL风格的证伪框架，该框架对每个量子比特的Bloch球面进行有限划分，同时一个可靠的理论求解器通过每个约束的投影振幅的几何过近似来检查区域可行性。当理论求解器证明某个区域中不存在任何状态能满足某个约束时，它会产生一个可靠的冲突子句来阻止该区域；累积的阻止子句可以得出乘积态不可满足性的全局结果（UN-PRODSAT）。我们对该问题进行了形式化描述，证明了子句学习规则的可靠性，并给出了实用的算法及实现。