{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreid6exljmcrjzkwvbrkbyb74eif3uwnuje76sjhbx3qy7eqzwyztty",
    "uri": "at://did:plc:3fychdutjjusoqeq24ljch6q/app.bsky.feed.post/3mhp6ricwyiw2"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreiflo6xt7is6b2iafwghkjahlgggocme5jwjsbeuqqwcywuvjhmszm"
    },
    "mimeType": "image/png",
    "size": 24783
  },
  "path": "/abs/2603.20038v1",
  "publishedAt": "2026-03-23T00:00:00.000Z",
  "site": "https://arxiv.org",
  "tags": [
    "Samuel González-Castillo",
    "Joon Hyung Lee",
    "Alfons Laarman"
  ],
  "textContent": "**Authors:** Samuel González-Castillo, Joon Hyung Lee, Alfons Laarman\n\nWe 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)"
}