From Leaves to Clusters: Depth-Efficient SAT-Oracle Synthesis Based on the FORM Model
Abstract
Quantum oracles play a fundamental role in many quantum algorithms, such as Grover's search and quantum counting. In oracle synthesis, reducing the circuit depth under a limited number of ancilla qubits is essential, given the constraints of current quantum devices. However, for satisfiability oracles (SAT-oracles) under a limited ancilla budget, existing synthesis methods fail to fully exploit clause-level parallelism, leading to deep circuits. In practice, evaluating clauses in parallel can quickly exhaust the ancilla budget. To address this issue, we introduce the Clustered Synthesis Tree (CST), a depth-oriented SAT-oracle synthesis framework that exploits clause-level parallelism while respecting the ancilla budget. CST leverages a recursive synthesis tree as the backbone for scheduling clause evaluations and groups its clause leaves into clusters, whose clauses are evaluated in parallel by a reversible oracle called ClausePack. To form the clusters, CST introduces a polynomial-time heuristic called SeedGrow for the NP-hard clause-grouping problem, and the resulting tree is compiled into an executable circuit by CST-Map. Compared with the depth-oriented pAND baseline, CST can reduce the circuit depth by an average of 10.2x and 8.8x-11.0x on SATLIB and random 4-CNF benchmarks, respectively, under the same ancilla budgets, while also outperforming the width-oriented pAND, clause-storing, and qSAT baselines.
Related
BibTeX
@misc{li2026from,
title = {{From Leaves to Clusters: Depth-Efficient SAT-Oracle Synthesis Based on the FORM Model}},
author = {Zhihang Li and Wei Zi and Shuai Yang and Bei Zhou and Zongjiang Yi and Woji He and Yingjie Lin and Kaixiang Ji and Heru Du and Jinchen Xu},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2607.11401},
eprint = {2607.11401},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2607.11401},
}
RIS
TY - UNPB
TI - From Leaves to Clusters: Depth-Efficient SAT-Oracle Synthesis Based on the FORM Model
AU - Zhihang Li
AU - Wei Zi
AU - Shuai Yang
AU - Bei Zhou
AU - Zongjiang Yi
AU - Woji He
AU - Yingjie Lin
AU - Kaixiang Ji
AU - Heru Du
AU - Jinchen Xu
PY - 2026
DA - 2026/10/27
PB - arXiv
DO - 10.48550/arxiv.2607.11401
UR - https://arxiv.org/abs/2607.11401
AB - Quantum oracles play a fundamental role in many quantum algorithms, such as Grover's search and quantum counting. In oracle synthesis, reducing the circuit depth under a limited number of ancilla qubits is essential, given the constraints of current quantum devices. However, for satisfiability oracles (SAT-oracles) under a limited ancilla budget, existing synthesis methods fail to fully exploit clause-level parallelism, leading to deep circuits. In practice, evaluating clauses in parallel can quickly exhaust the ancilla budget. To address this issue, we introduce the Clustered Synthesis Tree (CST), a depth-oriented SAT-oracle synthesis framework that exploits clause-level parallelism while respecting the ancilla budget. CST leverages a recursive synthesis tree as the backbone for scheduling clause evaluations and groups its clause leaves into clusters, whose clauses are evaluated in parallel by a reversible oracle called ClausePack. To form the clusters, CST introduces a polynomial-time heuristic called SeedGrow for the NP-hard clause-grouping problem, and the resulting tree is compiled into an executable circuit by CST-Map. Compared with the depth-oriented pAND baseline, CST can reduce the circuit depth by an average of 10.2x and 8.8x-11.0x on SATLIB and random 4-CNF benchmarks, respectively, under the same ancilla budgets, while also outperforming the width-oriented pAND, clause-storing, and qSAT baselines.
ER -