SAQC: A SAT-Aware Compilation Framework for QAOA-Based Quantum Optimization
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
- A Platform-aware Compilation Framework for Fault-tolerant Quantum Computation
- C-Phase-Aware Compilation for Efficient Fault-Tolerant Quantum Execution
- Decoder- and Noise-Aware Optimization Framework for Clifford-Deformed Quantum Error-Correcting Codes
- Local Automorphism-Aware Syndrome Compilation for General Quantum LDPC Codes
- A Compilation Framework for Quantum Simulation of Non-unitary Dynamics
BibTeX
@misc{schnittka2026saqc,
title = {{SAQC: A SAT-Aware Compilation Framework for QAOA-Based Quantum Optimization}},
author = {Till Schnittka and Julie Maria Raju and Abhoy Kole and Rolf Drechsler},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.05737},
eprint = {2609.05737},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.05737},
}
RIS
TY - UNPB
TI - SAQC: A SAT-Aware Compilation Framework for QAOA-Based Quantum Optimization
AU - Till Schnittka
AU - Julie Maria Raju
AU - Abhoy Kole
AU - Rolf Drechsler
PY - 2026
DA - 2026/09/09
PB - arXiv
DO - 10.48550/arxiv.2609.05737
UR - https://arxiv.org/abs/2609.05737
AB - 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.
ER -