Search-Driven Clause Learning for Product-State Quantum $k$-SAT (PRODSAT-QSAT)
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912976111403008 |
|---|---|
| author | González-Castillo, Samuel Lee, Joon Hyung Laarman, Alfons |
| author_facet | González-Castillo, Samuel Lee, Joon Hyung Laarman, Alfons |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_20038 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Search-Driven Clause Learning for Product-State Quantum $k$-SAT (PRODSAT-QSAT) González-Castillo, Samuel Lee, Joon Hyung Laarman, Alfons Quantum Physics Computational Complexity Logic in Computer Science 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. |
| title | Search-Driven Clause Learning for Product-State Quantum $k$-SAT (PRODSAT-QSAT) |
| topic | Quantum Physics Computational Complexity Logic in Computer Science |
| url | https://arxiv.org/abs/2603.20038 |