SAQC: A SAT-Aware Compilation Framework for QAOA-Based Quantum Optimization

• URL: http://arxiv.org/abs/2609.05737v2
• Date: Wed, 09 Sep 2026 10:10:33 GMT
• Title: SAQC: A SAT-Aware Compilation Framework for QAOA-Based Quantum Optimization
• Abstract summary: 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.
• Score: 1.214455026524814
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The Quantum Approximate Optimization Algorithm (QAOA) is a promising variational approach for solving Boolean satisfiability (SAT) problems. Existing SAT-to-QAOA workflows first translate Boolean formulas into penalty Hamiltonians before applying generic quantum compilation, thereby discarding SAT-specific information such as clause structure, logical operators, and variable dependencies. Consequently, subsequent compiler optimizations cannot exploit the underlying Boolean formulation. This paper presents SAQC, a SAT-aware compilation framework that introduces a SAT Intermediate Representation (SIR) to preserve Boolean structure during compilation. The proposed framework supports both CNF and XOR-extended CNF (eCNF) formulations and performs SAT-aware optimizations including clause rewriting, dependency analysis, and clause scheduling prior to quantum lowering. Building on the optimized SIR, SAQC provides a unified framework for both penalty Hamiltonian generation and direct clause-to-ansatz synthesis, together with ansatz optimizations based on relative-phase decomposition, ancilla-assisted synthesis, and dynamic uncomputation. Experimental results demonstrate significant reductions in circuit depth, two-qubit gate count, and compilation time compared with conventional Hamiltonian-based workflows while remaining compatible with existing quantum compilation frameworks.

Related papers

• Towards Tensor-Network SAT-Solvers for Quantum-Classical Workflows [1.1916225387199697]
  Integrated HPC/QC systems aim to combine classical high-performance computing with quantum processors.<n>An integrated architecture must support aspects such as observability, which cannot be implemented using QPUs alone.
  arXiv  Detail & Related papers  (2026-08-03T10:36:30Z)
• Performance Gains in Quantum SAT Solvers Using ESOP Encoding [1.3267048706241158]
  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.
  arXiv  Detail & Related papers  (2026-05-15T17:17:07Z)
• EQE-QAOA: An Equivalence-Preserving Qubit Efficient Framework for Combinatorial Optimization [54.05451096499336]
  Existing techniques rely on qubit reduction at the cost of information loss, leading to degraded computational performance.<n>We propose the Equivalence-preserving Qubit Efficient QAOA, which significantly reduces the required number of qubits without degrading performance.<n>We show that it is broadly applicable to large-scale optimization problems, excluding only unconstrained problems with completely independent variables.
  arXiv  Detail & Related papers  (2026-04-20T13:57:49Z)
• High-Performance Exact Synthesis of Two-Qubit Quantum Circuits [0.0]
  We present an exact synthesis framework for two-qubit circuits over the Clifford+$T$ gate set.<n>Our approach exhausts a bounded search space, exploits algebraic canonicalization to avoid redundancy, and constructs a lookup table of optimal implementations that turns synthesis into a query.
  arXiv  Detail & Related papers  (2026-01-27T03:57:04Z)
• FTCircuitBench: A Benchmark Suite for Fault-Tolerant Quantum Compilation and Architecture [9.755713238528779]
  FTCircuitBench serves as a benchmark suite of impactful quantum algorithms.<n>A modular end-to-end pipeline allows users to compile and decompose algorithms for various fault-tolerant architectures.<n>A toolkit provides detailed numerical analysis at each stage.
  arXiv  Detail & Related papers  (2026-01-06T17:08:46Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  We propose an end-to-end deep learning (DL) framework with low inference complexity for symbol-level precoding.<n>We show that the proposed framework captures substantial performance gains of optimal SLP, while achieving an approximately 80-times speedup over conventional methods.
  arXiv  Detail & Related papers  (2025-10-02T15:15:50Z)
• Direct phase encoding in QAOA: Describing combinatorial optimization problems through binary decision variables [0.7015624626359264]
  We show a more qubit-efficient circuit construction for optimization problems by the example of the Travelingperson Sales Problem (TSP)<n>Removing certain redundancies, the number of required qubits can be reduced by a linear factor compared to the aforementioned conventional encoding.<n>Our experiments show that for small instances results are just as accurate using our proposed encoding, whereas the number of required classical iterations increases only slightly.
  arXiv  Detail & Related papers  (2024-12-10T12:12:34Z)
• Provably Faster Algorithms for Bilevel Optimization via Without-Replacement Sampling [96.47086913559289]
  gradient-based algorithms are widely used in bilevel optimization. We introduce a without-replacement sampling based algorithm which achieves a faster convergence rate. We validate our algorithms over both synthetic and real-world applications.
  arXiv  Detail & Related papers  (2024-11-07T17:05:31Z)
• Tree ensemble kernels for Bayesian optimization with known constraints over mixed-feature spaces [54.58348769621782]
  Tree ensembles can be well-suited for black-box optimization tasks such as algorithm tuning and neural architecture search. Two well-known challenges in using tree ensembles for black-box optimization are (i) effectively quantifying model uncertainty for exploration and (ii) optimizing over the piece-wise constant acquisition function. Our framework performs as well as state-of-the-art methods for unconstrained black-box optimization over continuous/discrete features and outperforms competing methods for problems combining mixed-variable feature spaces and known input constraints.
  arXiv  Detail & Related papers  (2022-07-02T16:59:37Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Adaptive pruning-based optimization of parameterized quantum circuits [62.997667081978825]
  Variisy hybrid quantum-classical algorithms are powerful tools to maximize the use of Noisy Intermediate Scale Quantum devices. We propose a strategy for such ansatze used in variational quantum algorithms, which we call "Efficient Circuit Training" (PECT) Instead of optimizing all of the ansatz parameters at once, PECT launches a sequence of variational algorithms.
  arXiv  Detail & Related papers  (2020-10-01T18:14:11Z)

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.