Alfons Laarman

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 over-approximation of constraint amplitudes. When the checker proves that no state in a region can satisfy a constraint, it produces a sound conflict clause that blocks that region; accumulated learned 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.