Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Samuel González-Castillo, Joon Hyung Lee, Alfons Laarman

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.

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

Abstract

We study PRODSAT-QSAT(): given rank-one -local projectors, determine whether a quantum -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.
Paper Structure (11 sections, 8 theorems, 37 equations, 3 figures, 2 tables, 3 algorithms)

This paper contains 11 sections, 8 theorems, 37 equations, 3 figures, 2 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Problem definition.
  3. Contributions.
  4. Paper outline.
  5. Geometric preliminaries
  6. Theory solver
  7. Main architecture (Proof of Theorem \ref{['thm:main']})
  8. Additional hypotheses for PRODSAT results
  9. Regarding the need for a SAT solver
  10. Implementation
  11. Conclusions

Key Result

Theorem 1

Fix $k$ and consider a QSAT($k$) instance. Algorithm alg:full runs, in the worst-case scenario, in exponential time in the number of qubits. It returns UN-PRODSAT if it can certify that its input instance is UN-PRODSAT. Otherwise, it returns MAYBE($A$, $\rho$), where $A$ and $\rho$ are the sums of,

Figures (3)

  • Figure 1: Annular sectors, and their polygonal enclosures.
  • Figure 2: The black, red, blue and green segments are, respectively, the intervals $I()$, $I(0)$, $I(0,1)$ and $I(0,1,0)$. Each additional bit that is passed to $I$ represents a new step in a binary search through the interval $[0, 2\pi]$.
  • Figure 3: Evolution of the runtime of our implementation (average and standard deviation), with respect to the number of qubits. To give a fair representation, we only consider instances in which the number of constraints $m$ is equal to the number of qubits $n$.

Theorems & Definitions (17)

  • Definition 1: PRODSAT-QSAT($k$)
  • Theorem 1
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Definition 2
  • Lemma 3
  • proof
  • Remark 1
  • ...and 7 more