Search-Driven Clause Learning for Product-State Quantum $k$-SAT (PRODSAT-QSAT)

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.

Source: arXiv:2603.20038v1 - http://arxiv.org/abs/2603.20038v1 PDF: https://arxiv.org/pdf/2603.20038v1 Original Link: http://arxiv.org/abs/2603.20038v1