Pith. sign in

REVIEW 3 major objections 6 minor 25 references

Depth-Optimal Quantum Layout Synthesis as SAT

T0 review · 3 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A SAT encoding whose time steps equal circuit depth returns provably minimal-depth quantum layouts, and the paper shows exact depth-optimal transpilation is 10–100x faster than the prior SMT-based tool.

desk verdict First SAT encoding for depth-optimal layout synthesis with credible speedups and shipping code; completeness is asserted rather than proved, and the noise study is preliminary. read the letter →

arxiv 2506.06752 v1 pith:BGX754X5 submitted 2025-06-07 quant-ph cs.AI

Anna B. Jakobsen , Anders B. Clausen , Jaco van de Pol , Irfansha Shaik This is my paper
classification quant-phcs.AI
keywords quantumlayoutsynthesisSATencodingcircuitdepthCX-depthincrementalsolvingparallelplansnoisereductiontranspilation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tries to establish that exact, depth-optimal quantum layout synthesis—rewiring a logical circuit onto a hardware coupling map while preserving gate order—can be solved efficiently with a SAT encoding, implemented in the tool QuilLS. The encoding makes the number of parallel time layers equal the target circuit depth, so the first satisfiable bound is a guarantee of minimal depth or minimal CX-gate depth. On standard benchmarks, QuilLS solves far more instances than the previous exact tool OLSQ2 and is often more than 10–100x faster, though still slower than tools that minimize gate count. The paper also reports a counterintuitive empirical result: reducing CX-count correlates better with noise reduction than reducing depth, and combining CX-count with CX-depth gives the best noise reduction.

What carries the argument

The key machinery is a parallel-plan SAT encoding: each time layer holds independent gates acting on distinct qubits, so the number of layers equals the scheduled circuit's depth. The encoding introduces mapping variables, connectivity predicates, current/advanced/delayed gate flags, and swap variables that span three consecutive layers; a swap variable marks the final step of a SWAP and forces the mappings of the two physical qubits to exchange. An assumption variable enforces that no gate remains delayed at the final layer, and incremental SAT solving reuses learned clauses across increasing depth bounds, so the first satisfiable layer count is certified optimal.

What would settle it

Take a small circuit and coupling map (e.g., 4–6 qubits), enumerate all legal mapped circuits of depth at most t by brute force, and check whether QuilLS reports satisfiable exactly when such a circuit exists; any instance where brute force finds a depth-t circuit that the SAT encoding rejects would falsify the claimed optimality guarantee.

Watch

Extended reading notes

Core claim

The central discovery is a propositional encoding of quantum layout synthesis in which the makespan—the number of parallel time layers—directly equals the circuit's depth, with each SWAP gate spread over three consecutive layers and with mapping, connectivity, gate scheduling, and swap effects encoded by the constraint system. By testing satisfiability for increasing makespans starting from the input circuit's depth, the first satisfying assignment is a depth-optimal mapped circuit; preprocessing the circuit to only CX gates gives CX-depth-optimality. The paper claims this is the first SAT-based depth-optimal layout synthesizer, and that on 220 benchmark circuit–platform pairs it is often more than 10–100x faster than the SMT-based depth-optimal OLSQ2 while solving 78% of instances for depth and 84% for CX-depth, versus OLSQ2's 43% and 54%.

Load-bearing premise

That the SAT constraint system is complete: every legal mapped circuit of a given depth satisfies the constraints, so the first satisfiable depth bound is truly the minimum possible depth.

Editorial extensions

If this is right

  • Depth-optimal or CX-depth-optimal transpilation becomes practical for substantially more circuits: on the paper's benchmark set, QuilLS cuts timeouts from OLSQ2's 102–125 down to 35–48.
  • Because the first satisfiable depth is provably optimal, QuilLS can serve as a ground-truth baseline for evaluating heuristic mappers such as SABRE and near-optimal tools.
  • The local-SWAP-count variant produces depth-optimal circuits with a minimum number of SWAPs, giving a practical tradeoff point between depth and circuit size.
  • CX-depth optimization is faster than full depth optimization and, when preceded by a size-optimal pass, gives depths within 1–2% of optimal, making it a cheap default when only CX chains matter.
  • The empirical correlations suggest that optimizing CX-count together with CX-depth is the better objective for noise reduction, rather than depth alone.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Inference beyond the paper: if a formal soundness and completeness proof closes the gap the paper leaves open, the same three-layer SWAP encoding could be adapted to other native gate sets, since only the SWAP implementation block would change.
  • The reported absence of correlation between depth and noise suggests that plain circuit depth may not be a reliable proxy for decoherence; hardware-aware depth metrics that weight idle time could be more predictive. This is my interpretation, not the paper's claim.
  • A testable extension would add a weighted objective combining CX-count and CX-depth into the SAT makespan, automating the tradeoff the paper identifies as best for noise instead of treating them as separate optimization passes.
  • The brute-force falsifier described below could be packaged as a small validation suite for future layout-synthesis encodings, checking exact optimality on 4–6 qubit instances.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper presents QuilLS, a SAT-based tool for depth-optimal and CX-depth-optimal quantum layout synthesis. The encoding uses incremental SAT solving and parallel plans, with makespan corresponding to circuit depth, and introduces new constraints for scheduling three-step SWAP gates while preserving gate dependencies. The authors claim that the first satisfiable time step in Algorithm 1 yields a mapped circuit of minimal depth or minimal CX-depth, and report speedups of more than 10--100x over the SMT-based OLSQ2 tool on standard benchmarks. The paper also presents an experimental study comparing QuilLS with SABRE, Q-Synth, TB-OLSQ2, and OLSQ2, and an empirical analysis of how different optimization metrics (depth, CX-depth, CX-count) correlate with noise reduction in noisy simulations.

Significance. If the depth-optimality guarantee is formally established, this is a valuable contribution: it is the first SAT-based depth-optimal layout synthesizer, and the reported runtime improvements over OLSQ2 would make exact depth-optimal transpilation practical on substantially larger benchmarks. The paper is strong on the empirical side: it provides a reproducible implementation (GitHub, Zenodo), a broad benchmark suite across multiple platforms, and careful comparisons including locally minimal SWAP counts. The noise correlation study is interesting and appropriately framed as a preliminary empirical finding. The main weakness is that the central optimality claim is asserted rather than proved; a rigorous soundness and completeness argument for the encoding is needed before the 'guarantee' wording in the abstract is justified.

major comments (3)
  1. [Section 3, Algorithm 1] The paper asserts that "The first time step where the instance is satisfied is the optimal depth" (Section 3) and that the encoding "guarantees" minimal depth (abstract), but no soundness or completeness theorem is provided for constraints (1)--(20). A formal statement is needed: satisfiability of the constraint system at makespan t should be equivalent to existence of a legal mapped circuit of depth t, and the first satisfiable t in Algorithm 1 should be the true optimum. This is load-bearing because the central advertised guarantee depends on it, and the empirical agreement with OLSQ2 on shared benchmarks, while reassuring, does not cover all legal schedules, especially those involving interleaved or ancillary SWAPs.
  2. [Section 3, Eqs. (13)--(19)] The novel part of the encoding is the handling of three-step SWAPs, but completeness for this part is not argued. In particular, one must show that every legal depth-t mapped circuit, including circuits where SWAPs interleave with other gates on disjoint qubits and where an ancillary (single-occupied) SWAP is used, admits a satisfying assignment of constraints (13)--(19). Conversely, one must show that any satisfying assignment extracts to a valid mapped circuit respecting gate dependencies and connectivity. I recommend adding a proof by construction from an arbitrary feasible mapped circuit to a SAT assignment and the reverse extraction, or at minimum an exhaustive brute-force validation on all small circuits and coupling maps.
  3. [Section 3, Algorithm 1 and Section 3.1] The optimality claim also relies on monotonicity of satisfiability in the makespan t, so that padding a valid depth-t schedule to depth t+1 is always admitted by the constraints, and on monotonicity in the number of SWAPs for the locally minimal SWAP-count search in Section 3.1. Neither monotonicity property is proved; the latter is deferred to a citation [15]. These are elementary but should be stated explicitly, since Algorithm 1's loop otherwise could stop at a non-minimal t if the encoding rejected empty final layers or other padding schedules.
minor comments (6)
  1. [Algorithm 1] The pseudocode contains a typo: "Add M appingConstraints(t)" should be "Add MappingConstraints(t)".
  2. [References] References [22], [23], and [24] all point to the same paper (Tan and Cong, "Optimality study of existing quantum computing layout synthesis tools"); these should be consolidated into a single citation.
  3. [Section 4] The spelling of the SAT solver name is inconsistent: "CaDiCaL" appears in the tool list and references, while "CaDiCal" appears in the text; please unify.
  4. [Figure 3] The description of Figure 3 would benefit from stating explicitly what is plotted on each axis; currently the caption only says "time comparison" and the axes are not defined in the surrounding text.
  5. [Section 4.3] The noise-correlation results report correlation coefficients without confidence intervals or significance tests; given the small set of circuits and a single platform, a brief statement about variability would make the surprising absence of depth--noise correlation easier to interpret.
  6. [Section 3.1] The paper mentions that ancillary SWAPs can be disabled but only presents results with them allowed; a sentence on whether ancillary SWAPs actually occur in the reported solutions would clarify the practical relevance of this option.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the depth-optimality claim is benchmarked independently against OLSQ2, and no predicted quantity is fitted or defined by the paper's own outputs.

full rationale

The paper's central derivation is the SAT encoding of Section 3. The claim that the first satisfiable makespan is the optimal depth is semantic: Algorithm 1 tests t from 1 upward and returns the first t for which constraints (1)-(20) are satisfiable; if the constraints are sound and complete for 'there exists a legal mapped circuit of depth t', the first satisfiable t is optimal by definition. That soundness/completeness is not formally proved in the paper, but the absence of a proof is a correctness risk, not a circularity: the constraints are not defined in terms of the reported optimum, and no variable or clause is fitted to it. The paper's reuse of its own Q-Synth encoding (Section 3: 'Much of the structure of the encoding follows that of [20]') is a genuine self-citation, but it is not load-bearing for the depth-optimality contribution: the mapping and connectivity constraints are simple, Q-Synth is published and independently available, and the depth-optimal results are checked against the independent SMT tool OLSQ2. The noise-correlation study is empirical: Hellinger distances are simulated with Qiskit and correlated with reduction rates; no reduction rate or distance is used as a parameter in the encoding. Thus no derived quantity reduces by construction to an input or to the authors' own fitted values.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The central claim rests on standard assumptions about SWAP decomposition and circuit semantics, plus an unproved completeness premise for the SAT encoding. No new physical entities or fitted parameters are introduced; the remaining assumptions are modeling choices in the noise experiment.

assumptions (5)
  • domain assumption A SWAP gate can be implemented by exactly three CX gates and occupies three consecutive time steps on the swapped physical qubits.
    Used throughout Section 3, Equations 13-19, to schedule SWAPs over three layers and block gates on involved qubits. This is the standard decomposition, but it is an assumption about the hardware instruction set.
  • domain assumption The mapped circuit depth can never be smaller than the input circuit depth, so the search can start at t = depth(C).
    Algorithm 1 only tests makespans t >= D. This relies on the fact that adding SWAP gates cannot shorten the longest dependency chain of the input circuit.
  • ad hoc to paper The encoding is complete: every legal depth-t mapped circuit satisfies constraints (1)-(20).
    No formal soundness or completeness proof is given. The optimality guarantee depends on this unproved premise, which is the main correctness risk.
  • domain assumption The averaged Qiskit noise model with inserted idle I-gates is a faithful proxy for real device noise.
    Section 4.3 averages noise distributions over qubits and uses I-gate errors for decoherence. The noise-reduction conclusions depend on this proxy.
  • standard math Hellinger distance between ideal and noisy 100,000-shot simulations is a valid measure of circuit noise.
    Section 4.3 uses Qiskit simulations and Hellinger distance following Refs [4,7,18]. The choice of metric is standard in the cited literature.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Depth-Optimal Quantum Layout Synthesis as SAT." pith.science (2026). https://pith.science/paper/BGX754X5

@misc{pith2026250606752,
  author       = {Pith},
  title        = {Pith review of: Depth-Optimal Quantum Layout Synthesis as SAT},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BGX754X5}},
  note         = {Machine review of arXiv:2506.06752}
}
read the original abstract

Quantum circuits consist of gates applied to qubits. Current quantum hardware platforms impose connectivity restrictions on binary CX gates. Hence, Layout Synthesis is an important step to transpile quantum circuits before they can be executed. Since CX gates are noisy, it is important to reduce the CX count or CX depth of the mapped circuits. We provide a new and efficient encoding of Quantum-circuit Layout Synthesis in SAT. Previous SAT encodings focused on gate count and CX-gate count. Our encoding instead guarantees that we find mapped circuits with minimal circuit depth or minimal CX-gate depth. We use incremental SAT solving and parallel plans for an efficient encoding. This results in speedups of more than 10-100x compared to OLSQ2, which guarantees depth-optimality. But minimizing depth still takes more time than minimizing gate count with Q-Synth. We correlate the noise reduction achieved by simulating circuits after (CX)-count and (CX)-depth reduction. We find that minimizing for CX-count correlates better with reducing noise than minimizing for CX-depth. However, taking into account both CX-count and CX-depth provides the best noise reduction.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

25 extracted references · 7 canonical work pages

  1. [15]

    Scalable optimal layout synthesis for NISQ quantum processors

    Wan-Hsuan Lin, Jason Kimko, Bochen Tan, Nikolaj Bjørner, and Jason Cong. Scalable optimal layout synthesis for NISQ quantum processors. In DAC'23 , pages 1--6, 07 2023. https://doi.org/10.1109/DAC56929.2023.10247760 doi:10.1109/DAC56929.2023.10247760

    arXiv 2023

  2. [1]

    URL: https://docs.quantum.ibm.com/api/qiskit/qiskit.circuit.library.IGate

    Qiskit documentation. URL: https://docs.quantum.ibm.com/api/qiskit/qiskit.circuit.library.IGate

    work page

  3. [2]

    CaDiCaL , Kissat , Paracooba , Plingeling and Treengeling entering the SAT Competition 2020

    Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximilian Heisinger. CaDiCaL , Kissat , Paracooba , Plingeling and Treengeling entering the SAT Competition 2020 . In Proc. of SAT Competition 2020 -- Solver and Benchmark Descriptions , volume B-2020-1, pages 51--53. University of Helsinki, 2020. URL: https://api.semanticscholar.org/CorpusID:220727106

    work page 2020

  4. [3]

    Handbook of Satisfiability - Second Edition , volume 336 of Frontiers in Artificial Intelligence and Applications

    Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition , volume 336 of Frontiers in Artificial Intelligence and Applications . IOS Press, 2021

    work page 2021

  5. [4]

    Samudra Dasgupta and Travis S. Humble. Characterizing the reproducibility of noisy quantum circuits. Entropy , 24(2):244, February 2022. https://doi.org/10.3390/e24020244 doi:10.3390/e24020244

    doi:10.3390/e24020244 2022

  6. [5]

    Leonardo Mendon c a de Moura and Nikolaj S. Bj rner. Z3: an efficient SMT solver. In TACAS Proceedings , LNCS 4963, pages 337--340. Springer, 2008. https://doi.org/10.1007/978-3-540-78800-3\_24 doi:10.1007/978-3-540-78800-3\_24

    doi:10.1007/978-3-540-78800-3 2008

  7. [6]

    M. R. Garey, D. S. Johnson, and R. Endre Tarjan. The planar H amiltonian circuit problem is NP -complete. SIAM Journal on Computing , 5(4):704--714, 1976. https://doi.org/10.1137/0205049 doi:10.1137/0205049

    doi:10.1137/0205049 1976

  8. [7]

    Modeling and simulating the noisy behavior of near-term quantum computers

    Konstantinos Georgopoulos, Clive Emary, and Paolo Zuliani. Modeling and simulating the noisy behavior of near-term quantum computers. Physical Review A , 104(6), December 2021. https://doi.org/10.1103/physreva.104.062432 doi:10.1103/physreva.104.062432

    doi:10.1103/physreva.104.062432 2021

Show all 25 references
  1. [8]

    An efficient conversion of quantum circuits to a linear nearest neighbor architecture

    Yuichi Hirata, Masaki Nakanishi, Shigeru Yamashita, and Yasuhiko Nakashima. An efficient conversion of quantum circuits to a linear nearest neighbor architecture. Quantum Inf. Comput. , 11:142--166, 2011. https://doi.org/10.26421/QIC11.1-2-10 doi:10.26421/QIC11.1-2-10

    2011 doi

  2. [9]

    depth-optimal quantum layout synthesis as sat

    Anna Blume Jakobsen, Anders B. Clausen, J.C. van de Pol, and Irfansha Shaik. Code, benchmarks and data for "depth-optimal quantum layout synthesis as sat" paper at sat25, jun 2025. https://doi.org/10.5281/zenodo.15606051 doi:10.5281/zenodo.15606051

    2025 doi

  3. [10]

    Kautz, David A

    Henry A. Kautz, David A. McAllester, and Bart Selman. Encoding plans in propositional logic. In Proceedings of KR-96 , pages 374--384, November 1996. URL: https://henrykautz.com/papers/plankr96.pdf

    1996

  4. [11]

    M. S. Krishnamoorthy. An NP -hard problem in bipartite graphs. SIGACT News , 7(1):26, 1 1975. https://doi.org/10.1145/990518.990521 doi:10.1145/990518.990521

    1975

  5. [12]

    QASMBench : A low-level quantum benchmark suite for NISQ evaluation and simulation

    Ang Li, Samuel Stein, Sriram Krishnamoorthy, and James Ang. QASMBench : A low-level quantum benchmark suite for NISQ evaluation and simulation. ACM Transactions on Quantum Computing , 4(2), feb 2023. https://doi.org/10.1145/3550488 doi:10.1145/3550488

    2023 doi

  6. [13]

    Tackling the qubit mapping problem for nisq-era quantum devices

    Gushu Li, Yufei Ding, and Yuan Xie. Tackling the qubit mapping problem for nisq-era quantum devices. In ASPLOS , pages 1001--1014. ACM , 2019. https://doi.org/10.1145/3297858.3304023 doi:10.1145/3297858.3304023

    2019

  7. [16]

    Conflict-driven clause learning sat solvers

    Joao Marques-Silva, Ines Lynce, and Sharad Malik. Conflict-driven clause learning sat solvers. Handbook of Satisfiability , 336:133--182, 2021. https://doi.org/10.3233/FAIA200987 doi:10.3233/FAIA200987

    2021 doi

  8. [17]

    Nielsen and Isaac L

    Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information: 10th Anniversary Edition . Cambridge University Press, 2010

    2010

  9. [18]

    Karpuzcu

    Salonik Resch and Ulya R. Karpuzcu. Benchmarking quantum computers and the impact of quantum noise. ACM Comput. Surv. , 54(7):142:1--142:35, 2022. https://doi.org/10.1145/3464420 doi:10.1145/3464420

    2022 doi

  10. [19]

    Optimal layout synthesis for quantum circuits as classical planning

    Irfansha Shaik and Jaco van de Pol . Optimal layout synthesis for quantum circuits as classical planning. In 2023 IEEE/ACM International Conference on Computer Aided Design , ICCAD'23. IEEE, 2023. https://doi.org/10.1109/ICCAD57390.2023.10323924 doi:10.1109/ICCAD57390.2023.10323924

    2023

  11. [20]

    Optimal layout synthesis for deep quantum circuits on NISQ processors with 100+ qubits

    Irfansha Shaik and Jaco van de Pol. Optimal layout synthesis for deep quantum circuits on NISQ processors with 100+ qubits. In SAT'24 , volume 305, pages 26:1--18. LIPIcs, 2024. https://doi.org/10.4230/LIPIcs.SAT.2024.26 doi:10.4230/LIPIcs.SAT.2024.26

    2024 doi

  12. [21]

    t|ket⟩: a retargetable compiler for nisq devices

    Seyon Sivarajah, Silas Dilkes, Alexander Cowtan, Will Simmons, Alec Edgington, and Ross Duncan. t|ket⟩: a retargetable compiler for nisq devices. Quantum Science and Technology , 6(1):014003, November 2020. https://doi.org/10.1088/2058-9565/ab8e92 doi:10.1088/2058-9565/ab8e92

    2020 doi

  13. [23]

    Optimality study of existing quantum computing layout synthesis tools

    Bochen Tan and Jason Cong. Optimality study of existing quantum computing layout synthesis tools. IEEE Transactions on Computers , 70(9):1363–1373, September 2021. https://doi.org/10.1109/tc.2020.3009140 doi:10.1109/tc.2020.3009140

    2021

  14. [24]

    Mapping quantum circuits to IBM QX architectures using the minimal number of SWAP and H operations

    Robert Wille, Lukas Burgholzer, and Alwin Zulehner. Mapping quantum circuits to IBM QX architectures using the minimal number of SWAP and H operations. In Proceedings of the 56th Annual Design Automation Conference 2019 , DAC '19. ACM, June 2019. https://doi.org/10.1145/331678...

    2019

  15. [25]

    Chong, and Costin Iancu

    Xin-Chuan Wu, Marc Grau Davis, Frederic T. Chong, and Costin Iancu. Qgo: Scalable quantum circuit optimization using automated synthesis. 2022. https://arxiv.org/abs/2012.09835 arXiv:2012.09835

    2022 arXiv

  16. [26]

    Kharkov, Yunong Shi, Marijn J

    Jiong Yang, Yaroslav A. Kharkov, Yunong Shi, Marijn J. H. Heule, and Bruno Dutertre. Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving . In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) , volume 305 of Leibniz...

    2024 doi

  17. [27]

    An efficient methodology for mapping quantum circuits to the IBM QX architectures

    Alwin Zulehner, Alexandru Paler, and Robert Wille. An efficient methodology for mapping quantum circuits to the IBM QX architectures. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. , 38(7):1226--1236, 2019. https://doi.org/10.1109/TCAD.2018.2846658 doi:10.1109/TCAD.20...

    2019

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.