Performance Gains in Quantum SAT Solvers Using ESOP Encoding

• URL: http://arxiv.org/abs/2605.16202v1
• Date: Fri, 15 May 2026 17:17:07 GMT
• Title: Performance Gains in Quantum SAT Solvers Using ESOP Encoding
• Abstract summary: We investigate an Exclusive-Sum-of-Products-based CNF representation tailored for quantum SAT solving.<n>We derive tighter upper bounds on qubit requirements and Clifford+$T$ gate counts for Grover-based SAT solvers when e-CNF encodings are employed.<n> Experimental evaluation on representative SAT benchmarks demonstrates that the proposed e-CNF-based approach yields substantial and consistent reductions in quantum resources.
• Score: 1.3267048706241158
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The Boolean Satisfiability (SAT) problem is a canonical NP-complete problem and a natural candidate for quantum acceleration via search-based algorithms. In Grover-based quantum SAT solvers, the dominant computational cost stems from the construction of a reversible oracle that evaluates the Boolean formula, rendering the choice of SAT encoding crucial for overall quantum resource efficiency. Although SAT instances are conventionally expressed in Conjunctive Normal Form (CNF), such encodings typically translate into quantum circuits with significant qubit overhead and high non-Clifford gate complexity. In this work, we investigate an Exclusive-Sum-of-Products (ESOP)-based CNF (e-CNF) representation tailored for quantum SAT solving and analyze its impact on oracle construction. We derive tighter upper bounds on qubit requirements and Clifford+$T$ gate counts for Grover-based SAT solvers when e-CNF encodings are employed in place of standard CNF. In addition, we propose a scalable transformation from Boolean formulas to e-CNF and present a systematic procedure for interpreting e-CNF representations as reversible quantum circuits suitable for oracle implementation. Experimental evaluation on representative SAT benchmarks demonstrates that the proposed e-CNF-based approach yields substantial and consistent reductions in quantum resources, including qubit count, T-gate complexity, and circuit depth, when compared to CNF-based oracle constructions. These results establish e-CNF as an effective quantum-aware SAT encoding that significantly improves the practicality of oracle-based quantum SAT solving.

Related papers

• SAQC: A SAT-Aware Compilation Framework for QAOA-Based Quantum Optimization [1.214455026524814]
  This paper presents SAQC, a SAT-aware compilation framework that introduces a SAT Intermediate Representation (SIR) to preserve Boolean structure during compilation.<n>Building on the optimized SIR, SAQC provides a unified framework for both penalty Hamiltonian generation and direct clause-to-ansatz synthesis.<n> Experimental results demonstrate significant reductions in circuit depth, two-qubit gate count, and compilation time compared with conventional Hamiltonian-based synthesis.
  arXiv  Detail & Related papers  (2026-09-04T21:38:35Z)
• Verifiable quantum advantage in extremely low depth [52.51019642214249]
  We give a problem that is solvable by shallow quantum circuits, hard for computation in time under lattice-based assumptions.<n>We prove that shallow quantum circuits have sufficient structure to solve certain classically hard tasks whose solutions can be verified efficiently.
  arXiv  Detail & Related papers  (2026-09-01T15:54:34Z)
• Q-LEAK: Quantum-Based LEAKage Verification for Side-Channel Countermeasures [2.5435687567731926]
  We propose Q-LEAK, a quantum-based verification approach using Grover's algorithm.<n>Q-LEAK consistently recovered a satisfying assignment within 1-4 tries, with marked bitstrings amplified clearly above the background distribution.<n>The evaluation of Q-LEAK on real quantum hardware revealed at least one classically verified SAT assignment, despite the presence of noise.
  arXiv  Detail & Related papers  (2026-05-25T11:36:19Z)
• EQISA: Energy-efficient Quantum Instruction Set Architecture using Sparse Dictionary Learning [0.7856998585396422]
  We introduce an energy-efficient quantum instruction set architecture (EQISA) that synthesizes quantum circuits in a discrete Solovay-Kitaev basis of fixed depth.<n>This approach is evaluated on benchmark quantum circuits demonstrating over 60% compression of quantum instruction streams across system sizes.
  arXiv  Detail & Related papers  (2026-03-21T04:42:10Z)
• Quantum Approximate Optimization Algorithm for MIMO with Quantized b-bit Beamforming [47.98440449939344]
  Multiple-input multiple-output (MIMO) is critical for 6G communication, offering improved spectral efficiency and reliability.<n>This paper explores the use of the Quantum Approximate Optimization Algorithm (QAOA) and alternating optimization to address the problem of b-bit quantized phase shifters both at the transmitter and the receiver.<n>We demonstrate that the structure of this quantized beamforming problem aligns naturally with hybrid-classical methods like QAOA, as the phase shifts used in beamforming can be directly mapped to rotation gates in a quantum circuit.
  arXiv  Detail & Related papers  (2025-10-07T17:53:02Z)
• RhoDARTS: Differentiable Quantum Architecture Search with Density Matrix Simulations [44.13836547616739]
  Variational Quantum Algorithms (VQAs) are a promising approach to leverage Noisy Intermediate-Scale Quantum (NISQ) computers.<n> choosing optimal quantum circuits that efficiently solve a given VQA problem is a non-trivial task.<n>Quantum Architecture Search (QAS) algorithms enable automatic generation of quantum circuits tailored to the provided problem.
  arXiv  Detail & Related papers  (2025-06-04T08:30:35Z)
• qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking [2.178037930899554]
  We have proposed an efficient quantum SAT solver for equivalence checking of circuits employing Grover's algorithm. The Exclusive-Sum-of-Product based generation of the Conjunctive Normal Form equivalent clauses demand less qubits and minimizes the gates and depth of quantum circuit interpretation.
  arXiv  Detail & Related papers  (2024-09-05T21:25:38Z)
• Quantum Approximate Optimisation for Not-All-Equal SAT [9.427635404752936]
  We apply variational quantum algorithm QAOA to a variant of satisfiability problem (SAT): Not-All-Equal SAT. We show that while the runtime of both solvers scales exponentially with the problem size, the scaling for QAOA is smaller for large enough circuit depths.
  arXiv  Detail & Related papers  (2024-01-05T15:11:24Z)
• Qubit efficient quantum algorithms for the vehicle routing problem on NISQ processors [48.68474702382697]
  Vehicle routing problem with time windows (VRPTW) is a common optimization problem faced within the logistics industry. In this work, we explore the use of a previously-introduced qubit encoding scheme to reduce the number of binary variables.
  arXiv  Detail & Related papers  (2023-06-14T13:44:35Z)
• Quantum Annealing for Single Image Super-Resolution [86.69338893753886]
  We propose a quantum computing-based algorithm to solve the single image super-resolution (SISR) problem. The proposed AQC-based algorithm is demonstrated to achieve improved speed-up over a classical analog while maintaining comparable SISR accuracy.
  arXiv  Detail & Related papers  (2023-04-18T11:57:15Z)
• Decomposition of Matrix Product States into Shallow Quantum Circuits [62.5210028594015]
  tensor network (TN) algorithms can be mapped to parametrized quantum circuits (PQCs) We propose a new protocol for approximating TN states using realistic quantum circuits. Our results reveal one particular protocol, involving sequential growth and optimization of the quantum circuit, to outperform all other methods.
  arXiv  Detail & Related papers  (2022-09-01T17:08:41Z)
• Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond [3.610459670994051]
  We propose a propositional SAT encoding that can be applied to arbitrary quantum circuits. We show that due to the inherent complexity of representing quantum states, constructing such an encoding is not feasible in general. We explicitly demonstrate how the proposed encoding can be applied to the class of Clifford circuits as a representative.
  arXiv  Detail & Related papers  (2022-03-01T19:00:02Z)
• Resource Optimisation of Coherently Controlled Quantum Computations with the PBS-calculus [55.2480439325792]
  Coherent control of quantum computations can be used to improve some quantum protocols and algorithms. We refine the PBS-calculus, a graphical language for coherent control inspired by quantum optics.
  arXiv  Detail & Related papers  (2022-02-10T18:59:52Z)
• A Quantum-Inspired Classical Solver for Boolean k-Satisfiability Problems [0.0]
  We describe an algorithmic approach to the k-satisfiability (k-SAT) problem that is inspired by the amplification amplification algorithm. We then discuss meaningfully leveraging this setting in a classical digital or analog computing setting to identify the strengths and limitations of AmplifySAT.
  arXiv  Detail & Related papers  (2021-09-21T16:10:52Z)
• Quantum circuit architecture search for variational quantum algorithms [88.71725630554758]
  We propose a resource and runtime efficient scheme termed quantum architecture search (QAS) QAS automatically seeks a near-optimal ansatz to balance benefits and side-effects brought by adding more noisy quantum gates. We implement QAS on both the numerical simulator and real quantum hardware, via the IBM cloud, to accomplish data classification and quantum chemistry tasks.
  arXiv  Detail & Related papers  (2020-10-20T12:06:27Z)

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.