Search-Driven Clause Learning for Product-State Quantum $k$-SAT (PRODSAT-QSAT)
This addresses a computational problem in quantum computing for researchers studying quantum satisfiability, though it appears incremental as it adapts classical CDCL techniques to a quantum setting.
The paper tackles the problem of determining whether quantum k-SAT instances admit satisfying product states (PRODSAT-QSAT) by developing a CDCL-style refutation framework that searches finite partitions of qubit Bloch spheres and uses a geometric overapproximation to check constraint feasibility, resulting in a method that can prove product-state unsatisfiability (UN-PRODSAT).
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.