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

TL;DR

This paper introduces a search-driven clause learning framework for quantum $k$-SAT problems, enabling efficient determination of product-state satisfiability through geometric overapproximations and conflict clause learning.

Contribution

It presents a novel CDCL-style algorithm for PRODSAT-QSAT, combining geometric analysis with clause learning to decide product-state satisfiability.

Findings

Framework effectively identifies unsatisfiable instances

Soundness of the clause-learning rule is formally proven

Practical algorithm and implementation are described

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.