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

Synthesizing Circuits from Tableaus

anne mara

Published Jun 8, 2026• 0 citations
OpenAlex

Abstract

Quantum computers are only as powerful as the compilers that optimize the circuits they run. As quantum hardware scales, reducing gate counts and circuit depth becomes critical for practical computation. This work implements a core synthesis algorithm in OCaml that maps arbitrary Cliffords to circuits, a fundamental building block in quantum circuit compilation. The Clifford synthesis implementation is designed around how LambdaPC thinks about quantum computation, through Pauli operators. It frames synthesis as a search problem: given a Clifford tableau, find a path to the identity by applying gates. Working factor by factor, it reduces each Pauli pair (P, Q) to a canonical (Z_i, X_i) form using single-qubit Clifford gates and TQE gates, until the full tableau is decomposed into an executable circuit. The main challenge was working within LambdaPC's typed representation, where n-qubit Paulis are encoded as nested pairs. This required helper functions to extract Pauli data from those structures and pattern-matching logic to find minimal gate sequences, laying the groundwork for end-to-end Clifford compilation in LambdaPC.

Related papers

Architecture-Aware Synthesis of Stabilizer Circuits from Clifford Tableaus

David Winderl, Qunsheng Huang, Arianne Meijer-van de Griend +1 more

Since quantum computing is currently in the NISQ-Era, compilation strategies to reduce the number of gates executed on specific hardware are required. In this work, we utilize the concept of synthesis of a data structure called Clifford tableaus, focusing on applying CNOTs within the respective connectivity graph of the quantum device. We hence contribute to the field of compilation or, more precisely, synthesis by reducing the number of CNOTs in the synthesized quantum circuit. Upon convergence, our method shows to outperform other state-of-the-art synthesis techniques, when executed with respect to a specific hardware. Upon executing the resulting circuits on real hardware, our synthesized circuits tend to increase the final fidelity and reduce the overall execution times.

arXiv:2309.08972•Työväentutkimus Vuosikirja•Sep 16, 2023•2 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

A Simple Method for Compiling Quantum Stabilizer Circuits

Brendan Reid

Stabilizer circuits play an important role in quantum error correction protocols, and will be vital for ensuring fault tolerance in future quantum hardware. While stabilizer circuits are defined on the Clifford generating set,$\{H, S, CX\}$, not all of these gates are native to quantum hardware. As such they must be compiled into the native gateset, with the key difference across hardware archetypes being the native two-qubit gate. Here we introduce an intuitive and accessible method for Clifford gate compilation. While multiple open source solutions exist for quantum circuit compilation, these operate on arbitrary quantum gates. By restricting ourselves to Clifford gates, the compilation process becomes almost trivial and even large circuits can be compiled manually. The core idea is well known: if two Clifford circuits conjugate Paulis identically, they are equivalent. Compilation is then reduced to ensuring that the instantaneous Pauli conjugation is correct for each qubit at every timestep. This is Tableaux Manipulation, so called as we directly interrogate stabilizer tableaux to ensure correct Pauli conjugation. We provide a brief explanation of the process along with a worked example to build intuition; we finally show some comparisons for compiling large circuits to open source software, and highlight that this method ensures a minimal number of quantum gates are employed.

arXiv:2404.19408•IEEE International Conference on Quantum Computing and Engineering (QCE)•Sep 15, 2024•0 citations

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

Quantum Circuit Pre-Synthesis: Learning Local Edits to Reduce $T$-count

Daniele Lizzio Bosco, Lukasz Cincio, Giuseppe Serra +1 more

Compiling quantum circuits into Clifford+$T$ gates is a central task for fault-tolerant quantum computing using stabilizer codes. In the near term, $T$ gates will dominate the cost of fault tolerant implementations, and any reduction in the number of such expensive gates could mean the difference between being able to run a circuit or not. While exact synthesis is exponentially hard in the number of qubits, local synthesis approaches are commonly used to compile large circuits by decomposing them into substructures. However, composing local methods leads to suboptimal compilations in key metrics such as $T$-count or circuit depth, and their performance strongly depends on circuit representation. In this work, we address this challenge by proposing \textsc{Q-PreSyn}, a strategy that, given a set of local edits preserving circuit equivalence, uses a RL agent to identify effective sequences of such actions and thereby obtain circuit representations that yield a reduced $T$-count upon synthesis. Experimental results of our proposed strategy, applied on top of well-known synthesis algorithms, show up to a $20\%$ reduction in $T$-count on circuits with up to 25 qubits, without introducing any additional approximation error prior to synthesis.

quant-pharXiv:2601.19738•Jan 28, 2026•0 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
Quantum computers are only as powerful as the compilers that optimize the circuits they run. As quantum hardware scales, reducing gate counts and circuit depth becomes critical for practical computation. This work implements a core synthesis algorithm in OCaml that maps arbitrary Cliffords to circuits, a fundamental building block in quantum circuit compilation. The Clifford synthesis implementation is designed around how LambdaPC thinks about quantum computation, through Pauli operators. It frames synthesis as a search problem: given a Clifford tableau, find a path to the identity by applying gates. Working factor by factor, it reduces each Pauli pair (P, Q) to a canonical (Z_i, X_i) form using single-qubit Clifford gates and TQE gates, until the full tableau is decomposed into an executable circuit. The main challenge was working within LambdaPC's typed representation, where n-qubit Paulis are encoded as nested pairs. This required helper functions to extract Pauli data from those structures and pattern-matching logic to find minimal gate sequences, laying the groundwork for end-to-end Clifford compilation in LambdaPC.
Since quantum computing is currently in the NISQ-Era, compilation strategies to reduce the number of gates executed on specific hardware are required. In this work, we utilize the concept of synthesis of a data structure called Clifford tableaus, focusing on applying CNOTs within the respective connectivity graph of the quantum device. We hence contribute to the field of compilation or, more precisely, synthesis by reducing the number of CNOTs in the synthesized quantum circuit. Upon convergence, our method shows to outperform other state-of-the-art synthesis techniques, when executed with respect to a specific hardware. Upon executing the resulting circuits on real hardware, our synthesized circuits tend to increase the final fidelity and reduce the overall execution times.
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.
Stabilizer circuits play an important role in quantum error correction protocols, and will be vital for ensuring fault tolerance in future quantum hardware. While stabilizer circuits are defined on the Clifford generating set,{H,S,CX}\{H, S, CX\}{H,S,CX}, not all of these gates are native to quantum hardware. As such they must be compiled into the native gateset, with the key difference across hardware archetypes being the native two-qubit gate. Here we introduce an intuitive and accessible method for Clifford gate compilation. While multiple open source solutions exist for quantum circuit compilation, these operate on arbitrary quantum gates. By restricting ourselves to Clifford gates, the compilation process becomes almost trivial and even large circuits can be compiled manually. The core idea is well known: if two Clifford circuits conjugate Paulis identically, they are equivalent. Compilation is then reduced to ensuring that the instantaneous Pauli conjugation is correct for each qubit at every timestep. This is Tableaux Manipulation, so called as we directly interrogate stabilizer tableaux to ensure correct Pauli conjugation. We provide a brief explanation of the process along with a worked example to build intuition; we finally show some comparisons for compiling large circuits to open source software, and highlight that this method ensures a minimal number of quantum gates are employed.
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.
Quantum Circuit Pre-Synthesis: Learning Local Edits to Reduce TTT-count
Compiling quantum circuits into Clifford+TTT gates is a central task for fault-tolerant quantum computing using stabilizer codes. In the near term, TTT gates will dominate the cost of fault tolerant implementations, and any reduction in the number of such expensive gates could mean the difference between being able to run a circuit or not. While exact synthesis is exponentially hard in the number of qubits, local synthesis approaches are commonly used to compile large circuits by decomposing them into substructures. However, composing local methods leads to suboptimal compilations in key metrics such as TTT-count or circuit depth, and their performance strongly depends on circuit representation. In this work, we address this challenge by proposing \textsc{Q-PreSyn}, a strategy that, given a set of local edits preserving circuit equivalence, uses a RL agent to identify effective sequences of such actions and thereby obtain circuit representations that yield a reduced TTT-count upon synthesis. Experimental results of our proposed strategy, applied on top of well-known synthesis algorithms, show up to a 20%20\%20% reduction in TTT-count on circuits with up to 25 qubits, without introducing any additional approximation error prior to synthesis.
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.