Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Proceedings of the International Conference on Automated Planning and Scheduling

Optimal Clifford Synthesis as Planning

Irfansha Shaik, Jaco van de Pol

Published Jun 8, 2026• 0 citations
Publisher

Abstract

With the growing interest in practical quantum computing on noisy quantum hardware, quantum circuit optimization is becoming increasingly important. We consider the optimal synthesis of Clifford circuits, which are important for quantum error correction. While a scalable SAT encoding for Clifford synthesis exists, it only optimizes for the most noisy, i.e., binary quantum gates. That solution tends to add too many unary gates, thus introducing unnecessary noise sources. In this paper, we aim at synthesizing Clifford circuits with minimal binary gate count, and minimal unary gate count as a secondary optimization criterion. Expressing this in a performant SAT encoding is non-trivial. It turns out that planning specifications using PDDL with conditional effects are elegant and allow a flexible specification of costs. However, existing planners struggle on domains with conditional effects. The contribution of this paper is a number of different planning domains to solve the optimal binary/unary Clifford synthesis problem. The best performing solution combines the SAT approach for binary gates with a planning approach for unary gate minimization. As far as we know, this is the first approach that optimizes unary gates without increasing the binary gate count for Clifford circuits. With this hybrid approach, we present improved circuits for famous quantum error correcting codes, such as the Shor code and the Steane code. We believe that our various planning domains with conditional effects and costs form a challenging benchmark for contemporary planners.

DOI
10.1609/icaps.v36i1.42836

Related papers

A SAT Encoding for Optimal Clifford Circuit Synthesis

Sarah Schneider, Lukas Burgholzer, Robert Wille

Executing quantum algorithms on a quantum computer requires compilation to representations that conform to all restrictions imposed by the device. Due to devices' limited coherence times and gate fidelities, the compilation process has to be optimized as much as possible. To this end, an algorithm's description first has to be synthesized using the device's gate library. In this paper, we consider the optimal synthesis of Clifford circuits---an important subclass of quantum circuits, with various applications. Such techniques are essential to establish lower bounds for (heuristic) synthesis methods and gauging their performance. Due to the huge search space, existing optimal techniques are limited to a maximum of six qubits. The contribution of this work is twofold: First, we propose an optimal synthesis method for Clifford circuits based on encoding the task as a satisfiability (SAT) problem and solving it using a SAT solver in conjunction with a binary search scheme. The resulting tool is demonstrated to synthesize optimal circuits for up to 26 qubits---more than four times as many as the current state of the art. Second, we experimentally show that the overhead introduced by state-of-the-art heuristics exceeds the lower bound by 27 % on average. The resulting tool is publicly available at https://github.com/cda-tum/qmap.

arXiv:2208.11713•Asia and South Pacific Design Automation Conference (ASP-DAC)•Jan 16, 2023•17 citations

CNOT-Optimal Clifford Synthesis as SAT

Irfansha Shaik, Jaco van de Pol

Clifford circuit optimization is an important step in the quantum compilation pipeline. Major compilers employ heuristic approaches. While they are fast, their results are often suboptimal. Minimization of noisy gates, like 2-qubit CNOT gates, is crucial for practical computing. Exact approaches have been proposed to fill the gap left by heuristic approaches. Among these are SAT based approaches that optimize gate count or depth, but they suffer from scalability issues. Further, they do not guarantee optimality on more important metrics like CNOT count or CNOT depth. A recent work proposed an exhaustive search only on Clifford circuits in a certain normal form to guarantee CNOT count optimality. But an exhaustive approach cannot scale beyond 6 qubits. In this paper, we incorporate search restricted to Clifford normal forms in a SAT encoding to guarantee CNOT count optimality. By allowing parallel plans, we propose a second SAT encoding that optimizes CNOT depth. By taking advantage of flexibility in SAT based approaches, we also handle connectivity restrictions in hardware platforms, and allow for qubit relabeling. We have implemented the above encodings and variations in our open source tool Q-Synth. In experiments, our encodings significantly outperform existing SAT approaches on random Clifford circuits. We consider practical VQE and Feynman benchmarks to compare with TKET and Qiskit compilers. In all-to-all connectivity, we observe reductions up to 32.1% in CNOT count and 48.1% in CNOT depth. Overall, we observe better results than TKET in the CNOT count and depth. We also experiment with connectivity restrictions of major quantum platforms. Compared to Qiskit, we observe up to 30.3% CNOT count and 35.9% CNOT depth further reduction.

arXiv:2504.00634•Leibniz international proceedings in informatics•Jan 1, 2025•0 citations

Depth-Optimal Synthesis of Clifford Circuits with SAT Solvers

Tom Peham, Nina Brandl, Richard Kueng +2 more

Circuit synthesis is the task of decomposing a given logical functionality into a sequence of elementary gates. It is (depth-)optimal if it is impossible to achieve the desired functionality with even shorter circuits. Optimal synthesis is a central problem in both quantum and classical hardware design, but also plagued by complexity-theoretic obstacles. Motivated by fault-tolerant quantum computation, we consider the special case of synthesizing blocks of Clifford unitaries. Leveraging entangling input stimuli and the stabilizer formalism allows us to reduce the Clifford synthesis problem to a family of poly-size satisfiability (SAT) problems - one for each target circuit depth. On a conceptual level, our result showcases that the Clifford synthesis problem is contained in the first level of the polynomial hierarchy (NP), while the classical synthesis problem for logical circuits is known to be complete for the second level of the polynomial hierarchy (Σp2). Based on this theoretical reduction, we formulate a SAT encoding for depth-optimal Clifford synthesis. We then employ SAT solvers to determine a satisfying assignment or to prove that no such assignment exists. From that, the shortest depth for which synthesis is still possible (optimality) as well as the actual circuit (synthesis) can be obtained. Empirical evaluations show that the optimal synthesis approach yields a substantial depth improvement for random Clifford circuits and Clifford+T circuits for Grover search.

arXiv:2305.01674•IEEE International Conference on Quantum Computing and Engineering (QCE)•Sep 17, 2023•15 citations

Link-middle-cut lower bounds for Clifford circuit synthesis

Søren Fuglede Jørgensen

Minimizing the number of CNOT gates required to synthesize a Clifford operator is a central problem in quantum circuit optimization. We extend the link--middle--cut (LMC) framework for linear reversible circuits to Clifford operators represented by binary symplectic tableaux. By introducing block-support connectivity graphs and determinantal invariants, we obtain efficiently computable lower bounds on ancilla-free CNOT complexity. We prove that these bounds are tight for qubit permutations: a permutation of $n$ qubits with $k$ cycles requires exactly $3(n-k)$ CNOT gates, even when arbitrary one-qubit Clifford gates are available. We also derive efficiently computable bounds for synthesis up to a permutation of the output qubits, corresponding to free qubit relabeling. Finally, we further demonstrate the utility of the bound by using it as an admissible heuristic for $A^*$-based Clifford synthesis and show that, on benchmark instances, the resulting search can prove optimality beyond what was possible with earlier SAT-based methods, and that it may be used in combination with earlier $A^*$ heuristics to improve the CNOT counts obtained through heuristic search.

quant-pharXiv:2609.16208•Sep 16, 2026•0 citations

Heuristic and Optimal Synthesis of CNOT and Clifford Circuits

Mark Webster, Stergios Koutsioumpas, Dan E. Browne

Efficiently implementing Clifford circuits is crucial for quantum error correction and quantum algorithms. Linear reversible circuits, equivalent to circuits composed of CNOT\xspace gates, have important applications in classical computing. In this work we present methods for CNOT\xspace and general Clifford circuit synthesis which can be used to minimise either the entangling two-qubit gate count or the circuit depth. We present three families of algorithms - optimal synthesis which works on small circuits, A* synthesis for intermediate-size circuits and greedy synthesis for large circuits. We benchmark against existing methods, including rustiq, tket and qiskit and show that our approach results in circuits with lower two-qubit gate count. For encoding circuits, our methods outperform previous reinforcement learning results and find a lower two-qubit gate count circuit for the Golay code than previously known. The algorithms have been implemented in a GitHub repository for use by the classical and quantum computing community.

arXiv:2503.14660•Quantum•Sep 21, 2026•0 citations

Depth-Optimal Quantum Layout Synthesis as SAT

Anna Blume Jakobsen, Clausen, Anders B., Jaco van de Pol +1 more

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.

arXiv:2506.06752•Leibniz international proceedings in informatics•Jan 1, 2025•0 citations
With the growing interest in practical quantum computing on noisy quantum hardware, quantum circuit optimization is becoming increasingly important. We consider the optimal synthesis of Clifford circuits, which are important for quantum error correction. While a scalable SAT encoding for Clifford synthesis exists, it only optimizes for the most noisy, i.e., binary quantum gates. That solution tends to add too many unary gates, thus introducing unnecessary noise sources. In this paper, we aim at synthesizing Clifford circuits with minimal binary gate count, and minimal unary gate count as a secondary optimization criterion. Expressing this in a performant SAT encoding is non-trivial. It turns out that planning specifications using PDDL with conditional effects are elegant and allow a flexible specification of costs. However, existing planners struggle on domains with conditional effects. The contribution of this paper is a number of different planning domains to solve the optimal binary/unary Clifford synthesis problem. The best performing solution combines the SAT approach for binary gates with a planning approach for unary gate minimization. As far as we know, this is the first approach that optimizes unary gates without increasing the binary gate count for Clifford circuits. With this hybrid approach, we present improved circuits for famous quantum error correcting codes, such as the Shor code and the Steane code. We believe that our various planning domains with conditional effects and costs form a challenging benchmark for contemporary planners.
Executing quantum algorithms on a quantum computer requires compilation to representations that conform to all restrictions imposed by the device. Due to devices' limited coherence times and gate fidelities, the compilation process has to be optimized as much as possible. To this end, an algorithm's description first has to be synthesized using the device's gate library. In this paper, we consider the optimal synthesis of Clifford circuits---an important subclass of quantum circuits, with various applications. Such techniques are essential to establish lower bounds for (heuristic) synthesis methods and gauging their performance. Due to the huge search space, existing optimal techniques are limited to a maximum of six qubits. The contribution of this work is twofold: First, we propose an optimal synthesis method for Clifford circuits based on encoding the task as a satisfiability (SAT) problem and solving it using a SAT solver in conjunction with a binary search scheme. The resulting tool is demonstrated to synthesize optimal circuits for up to 26 qubits---more than four times as many as the current state of the art. Second, we experimentally show that the overhead introduced by state-of-the-art heuristics exceeds the lower bound by 27 % on average. The resulting tool is publicly available at https://github.com/cda-tum/qmap.
Clifford circuit optimization is an important step in the quantum compilation pipeline. Major compilers employ heuristic approaches. While they are fast, their results are often suboptimal. Minimization of noisy gates, like 2-qubit CNOT gates, is crucial for practical computing. Exact approaches have been proposed to fill the gap left by heuristic approaches. Among these are SAT based approaches that optimize gate count or depth, but they suffer from scalability issues. Further, they do not guarantee optimality on more important metrics like CNOT count or CNOT depth. A recent work proposed an exhaustive search only on Clifford circuits in a certain normal form to guarantee CNOT count optimality. But an exhaustive approach cannot scale beyond 6 qubits. In this paper, we incorporate search restricted to Clifford normal forms in a SAT encoding to guarantee CNOT count optimality. By allowing parallel plans, we propose a second SAT encoding that optimizes CNOT depth. By taking advantage of flexibility in SAT based approaches, we also handle connectivity restrictions in hardware platforms, and allow for qubit relabeling. We have implemented the above encodings and variations in our open source tool Q-Synth. In experiments, our encodings significantly outperform existing SAT approaches on random Clifford circuits. We consider practical VQE and Feynman benchmarks to compare with TKET and Qiskit compilers. In all-to-all connectivity, we observe reductions up to 32.1% in CNOT count and 48.1% in CNOT depth. Overall, we observe better results than TKET in the CNOT count and depth. We also experiment with connectivity restrictions of major quantum platforms. Compared to Qiskit, we observe up to 30.3% CNOT count and 35.9% CNOT depth further reduction.
Circuit synthesis is the task of decomposing a given logical functionality into a sequence of elementary gates. It is (depth-)optimal if it is impossible to achieve the desired functionality with even shorter circuits. Optimal synthesis is a central problem in both quantum and classical hardware design, but also plagued by complexity-theoretic obstacles. Motivated by fault-tolerant quantum computation, we consider the special case of synthesizing blocks of Clifford unitaries. Leveraging entangling input stimuli and the stabilizer formalism allows us to reduce the Clifford synthesis problem to a family of poly-size satisfiability (SAT) problems - one for each target circuit depth. On a conceptual level, our result showcases that the Clifford synthesis problem is contained in the first level of the polynomial hierarchy (NP), while the classical synthesis problem for logical circuits is known to be complete for the second level of the polynomial hierarchy (Σp2). Based on this theoretical reduction, we formulate a SAT encoding for depth-optimal Clifford synthesis. We then employ SAT solvers to determine a satisfying assignment or to prove that no such assignment exists. From that, the shortest depth for which synthesis is still possible (optimality) as well as the actual circuit (synthesis) can be obtained. Empirical evaluations show that the optimal synthesis approach yields a substantial depth improvement for random Clifford circuits and Clifford+T circuits for Grover search.
Minimizing the number of CNOT gates required to synthesize a Clifford operator is a central problem in quantum circuit optimization. We extend the link--middle--cut (LMC) framework for linear reversible circuits to Clifford operators represented by binary symplectic tableaux. By introducing block-support connectivity graphs and determinantal invariants, we obtain efficiently computable lower bounds on ancilla-free CNOT complexity. We prove that these bounds are tight for qubit permutations: a permutation of nnn qubits with kkk cycles requires exactly 3(n−k)3(n-k)3(n−k) CNOT gates, even when arbitrary one-qubit Clifford gates are available. We also derive efficiently computable bounds for synthesis up to a permutation of the output qubits, corresponding to free qubit relabeling. Finally, we further demonstrate the utility of the bound by using it as an admissible heuristic for A∗A^*A∗-based Clifford synthesis and show that, on benchmark instances, the resulting search can prove optimality beyond what was possible with earlier SAT-based methods, and that it may be used in combination with earlier A∗A^*A∗ heuristics to improve the CNOT counts obtained through heuristic search.
Efficiently implementing Clifford circuits is crucial for quantum error correction and quantum algorithms. Linear reversible circuits, equivalent to circuits composed of CNOT\xspace gates, have important applications in classical computing. In this work we present methods for CNOT\xspace and general Clifford circuit synthesis which can be used to minimise either the entangling two-qubit gate count or the circuit depth. We present three families of algorithms - optimal synthesis which works on small circuits, A* synthesis for intermediate-size circuits and greedy synthesis for large circuits. We benchmark against existing methods, including rustiq, tket and qiskit and show that our approach results in circuits with lower two-qubit gate count. For encoding circuits, our methods outperform previous reinforcement learning results and find a lower two-qubit gate count circuit for the Golay code than previously known. The algorithms have been implemented in a GitHub repository for use by the classical and quantum computing community.
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.