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

• URL: http://arxiv.org/abs/2603.20038v1
• Date: Fri, 20 Mar 2026 15:22:27 GMT
• Title: Search-Driven Clause Learning for Product-State Quantum $k$-SAT (PRODSAT-QSAT)
• Abstract summary: We study PRODSAT-QSAT($k$): given rank-one $k$-local projectors, determine whether a quantum $k$-SAT instance admits a satisfying product state.<n>We formalise the problem, prove the soundness of the clause-learning rule, and describe a practical algorithm and implementation.
• Score: 0.8301212911450326
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Tailoring Bell inequalities to the qudit toric code and self testing [0.0]
  We introduce a general framework for constructing Bell inequalities tailored to the $mathbbZ_d$ toric code for odd prime local dimensions.<n>We show that these inequalities are maximally violated by all states in the ground-state manifold of the $mathbbZ_d$ toric code.
  arXiv  Detail & Related papers  (2025-11-28T19:00:00Z)
• On the Probabilistic Learnability of Compact Neural Network Preimage Bounds [71.59148070050212]
  In this work, we adopt a novel probabilistic perspective, aiming to deliver solutions with high-confidence guarantees and bounded error.<n>We introduce $textbfR$andom $textbfF$orest $textbfPro$perty $textbfVe$rifier ($texttRF-ProVe$), a method that exploits an ensemble of randomized decision trees to generate candidate input regions satisfying a desired output property.<n>Our theoretical derivations offer formal statistical guarantees on region purity and global coverage, providing a practical, scalable solution for computing
  arXiv  Detail & Related papers  (2025-11-10T16:56:51Z)
• Provable Scaling Laws for the Test-Time Compute of Large Language Models [84.00141420901038]
  We propose two algorithms that enjoy provable scaling laws for the test-time compute of large language models.<n>One is a two-stage knockout-style algorithm, where each candidate is evaluated by its average win rate against multiple opponents.<n>The other is a two-stage league-style algorithm, where each candidate is evaluated by its average win rate against multiple opponents.
  arXiv  Detail & Related papers  (2024-11-29T05:29:47Z)
• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• The PRODSAT phase of random quantum satisfiability [7.5465062534540515]
  The $k$-QSAT problem is a quantum analog of the famous $k$-SAT constraint satisfaction problem. It is known that product states of zero energy exist with high probability if and only if the underlying factor graph has a clause-covering dimer configuration.
  arXiv  Detail & Related papers  (2024-04-29T06:10:45Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  We introduce the notion of decomposition hardness (d-hardness) We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
  arXiv  Detail & Related papers  (2023-12-16T12:44:36Z)
• Amplitude amplification-inspired QAOA: Improving the success probability for solving 3SAT [55.78588835407174]
  The amplitude amplification algorithm can be applied to unstructured search for satisfying variable assignments. The Quantum Approximate Optimization Algorithm (QAOA) is a promising candidate for solving 3SAT for Noisy Intermediate-Scale Quantum devices. We introduce amplitude amplification-inspired variants of QAOA to improve the success probability for 3SAT.
  arXiv  Detail & Related papers  (2023-03-02T11:52:39Z)
• Testing quantum satisfiability [0.0]
  We show that quantum k-SAT can be solved in randomised time.<n>We first show that for a satisfiable instance of quantum k-SAT, most subproblems on a constant number of qubits are satisfiable by a product state.<n>We then show that for an instance of quantum k-SAT which is far from satisfiable by a product state, most subproblems are unsatisfiable by a product state.
  arXiv  Detail & Related papers  (2023-01-25T17:02:46Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
  arXiv  Detail & Related papers  (2022-10-04T09:19:13Z)
• On Continuous Local BDD-Based Search for Hybrid SAT Solving [40.252804008544985]
  We propose a novel algorithm for efficiently computing the gradient needed by CLS. We study the capabilities and limitations of our versatile CLS solver, GradSAT, by applying it on many benchmark instances. The experimental results indicate that GradSAT can be a useful addition to the portfolio of existing SAT and MaxSAT solvers for solving Boolean satisfiability and optimization problems.
  arXiv  Detail & Related papers  (2020-12-14T22:36:20Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.