arXiv · 2603.20038
Search-Driven Clause Learning for Product-State Quantum $k$-SAT (PRODSAT-QSAT)
Abstract
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.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Samuel González-Castillo, Joon Hyung Lee, Alfons Laarman. 2026-03-20. Search-Driven Clause Learning for Product-State Quantum $k$-SAT (PRODSAT-QSAT). https://arxiv.org/abs/2603.20038
Cite the original work for its findings. Save a collection to share your selection of sources.