Repository: cda-tum/mqt-qmap (language: python)

Issue:
🎉 Core Functionality for Clifford Synthesis
## Description

This PR is the first in a series of feature PRs that tries to add the Clifford Synthesis functionality in a piece by piece fashion.
As a first step, the core functionality for synthesizing tableaus or optimizing circuits with optimal (two-qubit) gate count or depth is integrated and thoroughly tested.

## Checklist:

<!---
This checklist serves as a reminder of a couple of things that ensure your pull request will be merged swiftly.
-->

- [x] The pull request only contains commits that are related to it.
- [x] I have added appropriate tests and documentation.
- [x] I have made sure that all CI jobs on GitHub pass.
- [x] The pull request introduces no new warnings and follows the project's style guidelines.

Clifford synthesis
Adding the functionality to synthesize clifford circuits from tableaus and unoptimized input circuits, with some structural changes.

First, Adding LogicBlocks as a dependency and the logging functionality from there.
Introduction of Cliffordresults class to contain all Tableaus and Resulting Circuits.
Introduction of Tableaus as data structure to represent Clifford circuits.

ToDos:

- [x] Check integration of Logicblocks for sneaky errors 
- [x] Check functionality of Cliffordsynthesiszer
- [x] Write Tests for new Classes
- [x] Add ability to load a tableau from a tableau string as in qiskit (https://qiskit.org/documentation/stubs/qiskit.quantum_info.Clifford.html)
- [x] Add Python bindings


Discussion / hints:
pre-commit.ci run
# [Codecov](https://codecov.io/gh/cda-tum/qmap/pull/187?src=pr&el=h1&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum) Report
> Merging [#187](https://codecov.io/gh/cda-tum/qmap/pull/187?src=pr&el=desc&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum) (4202001) into [clifford_synthesis](https://codecov.io/gh/cda-tum/qmap/commit/da4ed69038db71d17f060c20c071769674a1b677?el=desc&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum) (da4ed69) will **increase** coverage by `1.6%`.
> The diff coverage is `97.4%`.

```diff
@@                 Coverage Diff                  @@
##           clifford_synthesis    #187     +/-   ##
====================================================
+ Coverage                92.1%   93.8%   +1.6%     
====================================================
  Files                      28      43     +15     
  Lines                    2493    3401    +908     
  Branches                  447     586    +139     
====================================================
+ Hits                     2297    3191    +894     
- Misses                    196     210     +14     
```

| Flag | Coverage Δ | |
|---|---|---|
| cpp | `93.6% <97.4%> (+2.0%)` | :arrow_up: |
| python | `95.3% <ø> (ø)` | |

Flags with carried forward coverage won't be shown. [Click here](https://docs.codecov.io/docs/carryforward-flags?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#carryforward-flags-in-the-pull-request-comment) to find out more.

| [Impacted Files](https://codecov.io/gh/cda-tum/qmap/pull/187?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum) | Coverage Δ | |
|---|---|---|
| [include/cliffordsynthesis/TargetMetric.hpp](https://codecov.io/gh/cda-tum/qmap/pull/187/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-aW5jbHVkZS9jbGlmZm9yZHN5bnRoZXNpcy9UYXJnZXRNZXRyaWMuaHBw) | `0.0% <0.0%> (ø)` | |
| [include/cliffordsynthesis/CliffordSynthesizer.hpp](https://codecov.io/gh/cda-tum/qmap/pull/187/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-aW5jbHVkZS9jbGlmZm9yZHN5bnRoZXNpcy9DbGlmZm9yZFN5bnRoZXNpemVyLmhwcA==) | `86.3% <86.3%> (ø)` | |
| [src/cliffordsynthesis/encoding/TableauEncoder.cpp](https://codecov.io/gh/cda-tum/qmap/pull/187/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-c3JjL2NsaWZmb3Jkc3ludGhlc2lzL2VuY29kaW5nL1RhYmxlYXVFbmNvZGVyLmNwcA==) | `91.0% <91.0%> (ø)` | |
| [...rc/cliffordsynthesis/encoding/ObjectiveEncoder.cpp](https://codecov.io/gh/cda-tum/qmap/pull/187/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-c3JjL2NsaWZmb3Jkc3ludGhlc2lzL2VuY29kaW5nL09iamVjdGl2ZUVuY29kZXIuY3Bw) | `94.4% <94.4%> (ø)` | |
| [src/cliffordsynthesis/CliffordSynthesizer.cpp](https://codecov.io/gh/cda-tum/qmap/pull/187/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-c3JjL2NsaWZmb3Jkc3ludGhlc2lzL0NsaWZmb3JkU3ludGhlc2l6ZXIuY3Bw) | `98.2% <98.2%> (ø)` | |
| [src/cliffordsynthesis/encoding/SATEncoder.cpp](https://codecov.io/gh/cda-tum/qmap/pull/187/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-c3JjL2NsaWZmb3Jkc3ludGhlc2lzL2VuY29kaW5nL1NBVEVuY29kZXIuY3Bw) | `98.8% <98.8%> (ø)` | |
| [include/cliffordsynthesis/Configuration.hpp](https://codecov.io/gh/cda-tum/qmap/pull/187/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-aW5jbHVkZS9jbGlmZm9yZHN5bnRoZXNpcy9Db25maWd1cmF0aW9uLmhwcA==) | `100.0% <100.0%> (ø)` | |
| [include/cliffordsynthesis/Results.hpp](https://codecov.io/gh/cda-tum/qmap/pull/187/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-aW5jbHVkZS9jbGlmZm9yZHN5bnRoZXNpcy9SZXN1bHRzLmhwcA==) | `100.0% <100.0%> (ø)` | |
| [include/cliffordsynthesis/encoding/GateEncoder.hpp](https://codecov.io/gh/cda-tum/qmap/pull/187/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-aW5jbHVkZS9jbGlmZm9yZHN5bnRoZXNpcy9lbmNvZGluZy9HYXRlRW5jb2Rlci5ocHA=) | `100.0% <100.0%> (ø)` | |
| [...de/cliffordsynthesis/encoding/ObjectiveEncoder.hpp](https://codecov.io/gh/cda-tum/qmap/pull/187/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-aW5jbHVkZS9jbGlmZm9yZHN5bnRoZXNpcy9lbmNvZGluZy9PYmplY3RpdmVFbmNvZGVyLmhwcA==) | `100.0% <100.0%> (ø)` | |
| ... and [17 more](https://codecov.io/gh/cda-tum/qmap/pull/187/diff?src=pr&el=tree-more&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum) | |

Help us with your feedback. Take ten seconds to tell us [how you rate us](https://about.codecov.io/nps?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum). Have a feature suggestion? [Share it here.](https://app.codecov.io/gh/feedback/?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum)

# [Codecov](https://codecov.io/gh/cda-tum/qmap/pull/78?src=pr&el=h1&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum) Report
> Merging [#78](https://codecov.io/gh/cda-tum/qmap/pull/78?src=pr&el=desc&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum) (7cd4e8a) into [main](https://codecov.io/gh/cda-tum/qmap/commit/baca8c6b0e3f626c63c525fef1905c84b36a379f?el=desc&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum) (baca8c6) will **increase** coverage by `0.5%`.
> The diff coverage is `93.7%`.

```diff
@@           Coverage Diff           @@
##            main     #78     +/-   ##
=======================================
+ Coverage   92.1%   92.7%   +0.5%     
=======================================
  Files         28      40     +12     
  Lines       2493    3444    +951     
  Branches     447     562    +115     
=======================================
+ Hits        2297    3193    +896     
- Misses       196     251     +55     
```

| Flag | Coverage Δ | |
|---|---|---|
| cpp | `92.3% <93.6%> (+0.7%)` | :arrow_up: |
| python | `95.4% <96.3%> (+0.1%)` | :arrow_up: |

Flags with carried forward coverage won't be shown. [Click here](https://docs.codecov.io/docs/carryforward-flags?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#carryforward-flags-in-the-pull-request-comment) to find out more.

| [Impacted Files](https://codecov.io/gh/cda-tum/qmap/pull/78?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum) | Coverage Δ | |
|---|---|---|
| [include/Architecture.hpp](https://codecov.io/gh/cda-tum/qmap/pull/78/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-aW5jbHVkZS9BcmNoaXRlY3R1cmUuaHBw) | `87.3% <ø> (+1.8%)` | :arrow_up: |
| [include/cliffordsynthesis/TargetMetric.hpp](https://codecov.io/gh/cda-tum/qmap/pull/78/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-aW5jbHVkZS9jbGlmZm9yZHN5bnRoZXNpcy9UYXJnZXRNZXRyaWMuaHBw) | `0.0% <0.0%> (ø)` | |
| [include/utils.hpp](https://codecov.io/gh/cda-tum/qmap/pull/78/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-aW5jbHVkZS91dGlscy5ocHA=) | `81.8% <ø> (+10.3%)` | :arrow_up: |
| [src/utils.cpp](https://codecov.io/gh/cda-tum/qmap/pull/78/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-c3JjL3V0aWxzLmNwcA==) | `77.2% <0.0%> (-14.5%)` | :arrow_down: |
| [include/cliffordsynthesis/OptimizationStrategy.hpp](https://codecov.io/gh/cda-tum/qmap/pull/78/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-aW5jbHVkZS9jbGlmZm9yZHN5bnRoZXNpcy9PcHRpbWl6YXRpb25TdHJhdGVneS5ocHA=) | `80.0% <80.0%> (ø)` | |
| [include/cliffordsynthesis/Gates.hpp](https://codecov.io/gh/cda-tum/qmap/pull/78/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-aW5jbHVkZS9jbGlmZm9yZHN5bnRoZXNpcy9HYXRlcy5ocHA=) | `81.4% <81.4%> (ø)` | |
| [src/cliffordsynthesis/ExactStrategy.cpp](https://codecov.io/gh/cda-tum/qmap/pull/78/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-c3JjL2NsaWZmb3Jkc3ludGhlc2lzL0V4YWN0U3RyYXRlZ3kuY3Bw) | `94.0% <94.0%> (ø)` | |
| [src/cliffordsynthesis/HeuristicStrategy.cpp](https://codecov.io/gh/cda-tum/qmap/pull/78/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-c3JjL2NsaWZmb3Jkc3ludGhlc2lzL0hldXJpc3RpY1N0cmF0ZWd5LmNwcA==) | `95.8% <95.8%> (ø)` | |
| [mqt/qmap/clifford\_synthesis.py](https://codecov.io/gh/cda-tum/qmap/pull/78/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-bXF0L3FtYXAvY2xpZmZvcmRfc3ludGhlc2lzLnB5) | `96.2% <96.2%> (ø)` | |
| [src/cliffordsynthesis/CliffordSynthesizer.cpp](https://codecov.io/gh/cda-tum/qmap/pull/78/diff?src=pr&el=tree&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum#diff-c3JjL2NsaWZmb3Jkc3ludGhlc2lzL0NsaWZmb3JkU3ludGhlc2l6ZXIuY3Bw) | `97.0% <97.0%> (ø)` | |
| ... and [13 more](https://codecov.io/gh/cda-tum/qmap/pull/78/diff?src=pr&el=tree-more&utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum) | |

Help us with your feedback. Take ten seconds to tell us [how you rate us](https://about.codecov.io/nps?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum). Have a feature suggestion? [Share it here.](https://app.codecov.io/gh/feedback/?utm_medium=referral&utm_source=github&utm_content=comment&utm_campaign=pr+comments&utm_term=cda-tum)

This pull request **introduces 3 alerts** when merging 195a3c033702bf689552f24ae36d60a3bc374fb9 into c1b13f966c10c4d876088788b6abb003098a6102 - [view on LGTM.com](https://lgtm.com/projects/g/cda-tum/qmap/rev/pr-b0252d5bbd2d43b986eb88452af3169d28712e1f)

**new alerts:**

* 2 for Overloaded assignment does not return &#39;this&#39;
* 1 for Multiplication result converted to larger type
This pull request **introduces 1 alert** when merging 25e5429b0ba8a310829809c9340fe02c23adb023 into c1b13f966c10c4d876088788b6abb003098a6102 - [view on LGTM.com](https://lgtm.com/projects/g/cda-tum/qmap/rev/pr-051bd7ec1ee7f4e0abaf4b0cb63481f7ed9dbec4)

**new alerts:**

* 1 for Overloaded assignment does not return &#39;this&#39;
This pull request **introduces 1 alert** when merging 5676cc6603e7a8f304574798cd2e30d65294753c into e8d1872f0d2160c412e1b29760c948a64399989f - [view on LGTM.com](https://lgtm.com/projects/g/cda-tum/qmap/rev/pr-6107c46b268149f30f107b256a36f9cd4ebd2119)

**new alerts:**

* 1 for Unused import
This pull request **introduces 1 alert** when merging 8f2cca4173741e1648da3c3ae848645590e83ae6 into e8d1872f0d2160c412e1b29760c948a64399989f - [view on LGTM.com](https://lgtm.com/projects/g/cda-tum/qmap/rev/pr-0767c6b725aa9a7827490e9f4da6001619bd8a07)

**new alerts:**

* 1 for Unused import
This pull request **introduces 2 alerts** when merging 55be705ed4150d16fd5b5f2ed7b88f54d3bf2d93 into e3c71c71dafa2c5f9277474dd03a38e73b579641 - [view on LGTM.com](https://lgtm.com/projects/g/cda-tum/qmap/rev/pr-5adfe5fb87c79a2f9534af69b7284367f3f41eb9)

**new alerts:**

* 2 for Unused import
This pull request **introduces 4 alerts** when merging 702274a30a0b2dcd2240a01c26ef7aed7b93551c into e3c71c71dafa2c5f9277474dd03a38e73b579641 - [view on LGTM.com](https://lgtm.com/projects/g/cda-tum/qmap/rev/pr-41747e57c444714f9223b23f699eb25c03b7af39)

**new alerts:**

* 2 for Unused local variable
* 2 for Multiplication result converted to larger type
This pull request **introduces 4 alerts** when merging a2306f820aaf09bd9ffa6eb3abafc199a965bc11 into c862346dcf05ce92fec8b1743ab4e1525842d529 - [view on LGTM.com](https://lgtm.com/projects/g/cda-tum/qmap/rev/pr-68ff90f1dc3e51ffa11e44ba257e7a868710b36e)

**new alerts:**

* 2 for Unused local variable
* 2 for Multiplication result converted to larger type
> This, again, is a rather incomplete review and includes comments on stuff that I stumbled upon while judging the current structure of the Clifford synthesis library.
> 
> I would propose the following structure (demonstrated here for the include files. the same applies to the src directory):
> 
> * include/cliffordsynthesis/
>   
>   * Tableau.hpp
>   * Configuration.hpp
>   * Method.hpp (preferably as "Engine.hpp" or "ReasoningEngine.hpp")
>   * Strategy.hpp (preferably as "OptimizationStrategy")
>   * Target.hpp (preferably as "TargetMetric.hpp")
>   * Results.hpp
> 
> All of these should contain structs/classes that have the same name as the file and be placed under a common namespace (to discern them from the mapping equivalents). The namespace could for example be `cs::` in order to stay with the two letter abbreviations (`dd`, `qc`, `ec`,... ). The namespace and placing everything in a common subfolder safes the annoying `Synthesis` prefix in all names.
> 
> As for the interesting part, i.e., the Synthesizer itself: I would definitely combine the `Synthesizer.hpp` and the `CliffordSynthesizer.hpp` files and classes. To be honest, I expected the splitting of the target metrics to have more of an effect. As of now, I does look like that hardly makes sense and the better solution is to combine all of it in the `CliffordSynthesizer.hpp`. Maybe it's possible to eliminate some of the code duplication between strategies and target metrics by factoring out something like "termination criterion", "stopping condition", etc.

There is hardly any code duplication anyway, most of that is refactored out into methods and functions already (SingleGate and MultiGateConstraints etc), but the next step would be factoring them out in Classes to have more smaller classes that each have one function that gets called? 
Combining all Strategies and Targets in one file makes sense, as does the introduction of a namespace. 
This pull request **introduces 2 alerts** when merging b8f9810d929cb8d57b9b883996c6d0582dc53eba into 1d3b759b3127f0b97aab52b6d61233e893b4166e - [view on LGTM.com](https://lgtm.com/projects/g/cda-tum/qmap/rev/pr-16f8a7ace52a97fabb1692e365046edcb9891233)

**new alerts:**

* 2 for Unused local variable
This pull request **introduces 2 alerts** when merging 5ea9680533f6eaa2d1755ac2d5a330b9e3278389 into 1d3b759b3127f0b97aab52b6d61233e893b4166e - [view on LGTM.com](https://lgtm.com/projects/g/cda-tum/qmap/rev/pr-06729a8fedf59d1a53f271e09324204f9387598b)

**new alerts:**

* 2 for Unused local variable
This pull request **introduces 3 alerts** when merging 5e49ae54136b395d498f04d096dd81c8be3d5d3b into 1d3b759b3127f0b97aab52b6d61233e893b4166e - [view on LGTM.com](https://lgtm.com/projects/g/cda-tum/qmap/rev/pr-c7c6a8b8f34fd636bab7bf0f092848ec822e21ab)

**new alerts:**

* 2 for Multiplication result converted to larger type
* 1 for Unused import
This is just a checkpoint for my in-depth look through the code. I started pretty much from the high level and began to refactor and fix certain parts as I stumbled upon them. Along the way I probably broke more things than I fixed, but I plan to continue working on the PR during the course of this week.

What I mainly did, was add some documentation of how I would like all the stuff to work at least from the minimal point of view of gate-optimal synthesis. Now I need some time to really dig deep into the code and see where some aspects can be improved.

I try to keep related changes in as small commits as possible so that the changes stay transparent.
Another checkpoint from my end. There are still lots of places in the code that need improvement.
Over the course of the past days, I discovered several subtle bugs in the implementation that were not covered by tests. Judging from the complexity of some of the functions and the lack of proper tests, I expect more of those in the code.

One conceptional thing I am still debating with myself:
the distinction between `synthesize` and `optimize` is so subtle, that it almost does not make sense and creates more duplication than it helps as a separation of concerns. 
In the very end, the best solution might be to have this distinction between optimization and synthesis _only_ in the end-user facing functions and unify the bindings as well as the C++ functions.

I'll continue working on this over the weekend.
Please resolve the conflicts in this PR so that CI is triggered properly.
Just merged in the newest changes from `main` and fixed a couple of bugs.
I am starting to factor out some changes from this PR into smaller PRs that can already be incorporated into `main` while the rest of the code is still being fixed.

The `mypy` job is currently failing since stubs for the synthesis functionality in the python bindings are missing from the newly introduced stubs file.

Fix patch:
diff --git a/.gitmodules b/.gitmodules
index 67b1bfd2f..6f282666e 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -5,6 +5,6 @@
     shallow = true
 [submodule "extern/LogicBlocks"]
 	path = extern/LogicBlocks
-	url = https://github.com/IsFairy/LogicBlocks.git
+	url = https://github.com/cda-tum/LogicBlocks.git
     branch = main
     shallow = true
diff --git a/README.md b/README.md
index d530d6cbd..502b49b12 100644
--- a/README.md
+++ b/README.md
@@ -18,7 +18,6 @@
 
 A tool for quantum circuit compilation developed as part of the _Munich Quantum Toolkit_ (_MQT_)[^1] by the [Chair for Design Automation](https://www.cda.cit.tum.de/) at the [Technical University of Munich](https://www.tum.de/).
 It builds upon [our quantum functionality representation (QFR)](https://github.com/cda-tum/qfr).
-.
 
 <p align="center">
   <a href="https://mqtqmap.readthedocs.io/en/latest/">
@@ -51,6 +50,21 @@ circ.cx(0, 2)
 circ_mapped, results = qmap.compile(circ, arch=FakeLondon())
 ```
 
+Optimizing a Clifford circuit is as easy as
+
+```python3
+from mqt import qmap
+from qiskit import QuantumCircuit
+
+circ = QuantumCircuit(2)
+circ.h(1)
+circ.cx(0, 1)
+circ.h(0)
+circ.h(1)
+
+circ_opt, results = qmap.optimize_clifford(circ)
+```
+
 **Detailed documentation on all available methods, options, and input formats is available at [ReadTheDocs](https://mqtqmap.readthedocs.io/en/latest/).**
 
 ## System Requirements and Building
@@ -83,4 +97,8 @@ _In Asia and South Pacific Design Automation Conference (ASP-DAC)_, 2022.
 T. Peham, L. Burgholzer, and R. Wille. On Optimal Subarchitectures for Quantum Circuit Mapping.
 _arXiv:2210.09321_, 2022.
 
+[[6]](https://arxiv.org/pdf/2208.11713.pdf)
+S. Schneider, L. Burgholzer, and R. Wille. A SAT Encoding for Optimal Clifford Circuit Synthesis.
+_In Asia and South Pacific Design Automation Conference (ASP-DAC)_, 2023.
+
 [^1]: The Munich Quantum Toolkit was formerly known under the acronym _JKQ_ and developed by the [Institute for Integrated Circuits](https://iic.jku.at/eda/) at the [Johannes Kepler University Linz](https://jku.at)).
diff --git a/docs/source/Publications.rst b/docs/source/Publications.rst
index 46ffc2345..ffcbe4c6a 100644
--- a/docs/source/Publications.rst
+++ b/docs/source/Publications.rst
@@ -3,7 +3,7 @@ Publications
 
 *QMAP* is academic software. Thus, many of its built-in algorithms have been published as scientific papers.
 
-If you use *QMAP* in your work, we would appreciate if you cited :cite:labelpar:`zulehnerEfficientMethodologyMapping2019` when using the heuristic mapper and :cite:labelpar:`willeMappingQuantumCircuits2019` when using the exact mapper.
+If you use *QMAP* in your work, we would appreciate if you cited :cite:labelpar:`zulehnerEfficientMethodologyMapping2019` when using the heuristic mapper, :cite:labelpar:`willeMappingQuantumCircuits2019` when using the exact mapper, and :cite:labelpar:`schneider2023satEncodingOptimalClifford` when using the Clifford circuit synthesis approach.
 Furthermore, if you use any of the particular algorithms such as
 
 - the heuristic mapping scheme using teleportation :cite:labelpar:`hillmichExlpoitingQuantumTeleportation2021`
diff --git a/docs/source/Synthesis.ipynb b/docs/source/Synthesis.ipynb
new file mode 100644
index 000000000..fc3082d41
--- /dev/null
+++ b/docs/source/Synthesis.ipynb
@@ -0,0 +1,178 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Synthesis of Clifford Circuits\n",
+    "\n",
+    "Executing quantum circuits on a quantum computer requires compilation to representations that conform to all restrictions imposed by the device.\n",
+    "Due to device's limited coherence times and gate fidelity, the compilation process has to be optimized as much as possible.\n",
+    "To this end, an algorithm's description first has to be *synthesized* using the device's gate library.\n",
+    "In addition, circuits have to be *mapped* to the target quantum device to satisfy its connectivity constraints.\n",
+    "Even though Clifford circuits form a finite subgroup of all quantum circuits -- one that is not even universal for quantum computing -- the search space for these problems grows exponentially with respect to the number of considered qubits.\n",
+    "\n",
+    "The *Clifford synthesis approach* in QMAP can be used to produce optimal Clifford circuits based on the methods proposed in <cite data-cite=\"schneider2023satEncodingOptimalClifford\">A SAT Encoding for Optimal Clifford Circuit Synthesis</cite>.\n",
+    "To this end, it encodes the underlying task as a satisfiability (SAT) problem and solves it using the [SMT solver Z3](https://github.com/Z3Prover/z3) in conjunction with a binary search scheme.\n",
+    "\n",
+    "The following gives a brief overview on Clifford circuits and how QMAP can be used for their synthesis."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Clifford Circuits\n",
+    "\n",
+    "Clifford circuits, i.e., circuits generated from the set $\\{H, S, \\mathit{CNOT}\\}$, form an important subclass of quantum circuits.\n",
+    "This is due to several factors\n",
+    "\n",
+    "- According to the Gottesman-Knill theorem, they can be simulated in polynomial time and space on classical computers using the *stabilizer* formalism.\n",
+    "- They can be used to describe several quantum phenomena such as superposition, entanglement, superdense coding, and teleportation.\n",
+    "- Many error correcting codes rely on them.\n",
+    "\n",
+    "Quantum states that can be obtained from the all-zero basis state $|0\\dots 0\\rangle$ by applying Clifford operations are called stabilizer states.\n",
+    "The name originates from the fact that such a state is uniquely and efficiently described by the set of operators that generate the group of its stabilizers.\n",
+    "Specifically, any *n*-qubit stabilizer state can be described by a set of *n* Pauli strings $\\pm P_{i,0}P_{i,1}P_{i,2}\\dots P_{i,n-1}$, with $P_{i,j}\\in\\{I, X, Y, Z\\}$ and $i, j\\in 0,\\dots, n-1$.\n",
+    "Hence,two bits per qubit are needed to identify the Pauli operator, as well as one additional bit for the phase, which leads to a total of $n(2n+1)` bits needed to uniquely describe a particular stabilizer state.\n",
+    "\n",
+    "The stabilizer representation of a quantum state is conveniently described by a *tableau*:\n",
+    "\n",
+    "$$\n",
+    "    \\begin{bmatrix}\n",
+    "        x_{0,0}   & \\cdots & x_{0,n-1}   & z_{0,0}    & \\cdots & z_{0,n-1}   & r_0    \\\\\n",
+    "        \\vdots    & \\ddots &  \\vdots         & \\vdots     & \\ddots &    \\vdots         & \\vdots \\\\\n",
+    "        x_{n-1,0} & \\cdots & x_{n-1,n-1} & z_{n-1,0} & \\cdots & z_{n-1,n-1} & r_{n-1}  \\\\\n",
+    "    \\end{bmatrix}\n",
+    "$$\n",
+    "\n",
+    "Here, the binary variables $x_{ij}$ and $z_{ij}$ specify whether the Pauli term $P_{i,j}$ is $X$ or $Z$, respectively.\n",
+    "Since $Y = iXZ$, setting $x_{ij} = z_{ij} = 1$ corresponds to $P_{i,j}=Y$.\n",
+    "Finally, $r_i$ describes whether the generator has a negative phase.\n",
+    "\n",
+    "Consider the following quantum circuit:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from qiskit import QuantumCircuit\n",
+    "\n",
+    "qc = QuantumCircuit(2)\n",
+    "qc.h(0)\n",
+    "qc.cx(0, 1)\n",
+    "qc.h(0)\n",
+    "qc.h(1)\n",
+    "\n",
+    "qc.draw(output=\"mpl\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "\n",
+    "Then, the corresponding stabilizer tableau is\n",
+    "\n",
+    "        0 0 | 1 1 | 0\n",
+    "        1 1 | 0 0 | 0\n",
+    "\n",
+    "which corresponds to the stabilizers"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "stabilizers = [\"+ZZ\", \"+XX\"]"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Using QMAP for Optimal Synthesis\n",
+    "\n",
+    "*QMAP* can be used in a multitude of ways to efficiently synthesize Clifford circuits:\n",
+    "\n",
+    "### Starting from an initial circuit `qc`"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from qiskit import QuantumCircuit\n",
+    "from mqt import qmap\n",
+    "\n",
+    "qc = QuantumCircuit(2)\n",
+    "qc.h(0)\n",
+    "qc.cx(0, 1)\n",
+    "qc.h(0)\n",
+    "qc.h(1)\n",
+    "\n",
+    "qc_opt, results = qmap.optimize_clifford(circuit=qc, use_maxsat=True)\n",
+    "\n",
+    "qc_opt.draw(output=\"mpl\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "### Starting from a functional description"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from mqt import qmap\n",
+    "\n",
+    "tableau = qmap.Tableau(\"['+ZZ', '+XX']\")\n",
+    "qc_synth, results = qmap.synthesize_clifford(tableau)\n",
+    "\n",
+    "qc_synth.draw(output=\"mpl\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "\n",
+    "The synthesis method offers lots of configuration options to fine-tune the synthesis procedure, e.g., changing the target metric.\n",
+    "\n",
+    "Check out the [reference documentation](library/Synthesis.rst) for more information."
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 2
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython2"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}
diff --git a/docs/source/index.rst b/docs/source/index.rst
index 11978fa25..6e5ac84b4 100644
--- a/docs/source/index.rst
+++ b/docs/source/index.rst
@@ -4,7 +4,7 @@ Welcome to QMAP's documentation!
 QMAP is a tool for quantum circuit compilation developed as part of the *Munich Quantum Toolkit* (*MQT*) [#]_ by the `Chair for Design Automation <https://www.cda.cit.tum.de/>`_ at the `Technical University of Munich <https://www.tum.de>`_. It builds upon `our quantum functionality representation (QFR) <https://github.com/cda-tum/qfr>`_.
 
 We recommend you to start with the :doc:`installation instructions <Installation>`.
-Then proceed to the :doc:`mapping page <Mapping>` and read the :doc:`reference documentation <library/Library>`.
+Then proceed to the :doc:`mapping page <Mapping>` or the :doc:`synthesis/optimization page <Synthesis>` and read the :doc:`reference documentation <library/Library>`.
 If you are interested in the theory behind QMAP, have a look at the publications in the :doc:`publication list <Publications>`.
 
 We appreciate any feedback and contributions to the project. If you want to contribute, you can find more information in the :doc:`Contribution <Contributing>` guide. If you are having trouble with the installation or the usage of QCEC, please let us know at our :doc:`Support <Support>` page or by reaching out to us at `quantum.cda@xcit.tum.de <mailto:quantum.cda@xcit.tum.de>`_.
@@ -23,6 +23,7 @@ We appreciate any feedback and contributions to the project. If you want to cont
 
     Installation
     Mapping
+    Synthesis
     Publications
 
 .. toctree::
diff --git a/docs/source/library/Library.rst b/docs/source/library/Library.rst
index 6f7cb5d69..6cd1f4f69 100644
--- a/docs/source/library/Library.rst
+++ b/docs/source/library/Library.rst
@@ -8,3 +8,5 @@ Library
    Architecture
    MappingResults
    Subarchitectures
+   Synthesis
+   SynthesisResults
diff --git a/docs/source/library/Synthesis.rst b/docs/source/library/Synthesis.rst
new file mode 100644
index 000000000..e69fd8a83
--- /dev/null
+++ b/docs/source/library/Synthesis.rst
@@ -0,0 +1,27 @@
+Quantum Circuit Synthesis
+=========================
+
+The main functionality for synthesizing quantum circuits is provided by the :func:`~mqt.qmap.synthesize_clifford` and the :func:`~mqt.qmap.optimize_clifford` methods.
+
+
+
+    .. currentmodule:: mqt.qmap
+    .. autofunction:: mqt.qmap::synthesize_clifford
+    .. autofunction:: mqt.qmap::optimize_clifford
+
+
+
+Synthesis Configuration
+#######################
+
+The following classes provide a more explicit way of initializing the respective parameters of the :code:`synthesize_clifford` and the :code:`optimize_clifford` method. Instead of setting parameters via :code:`str` members, they can be set with :code:`Enumeration.member` where :code:`Enumeration` is the enumeration class.
+
+    .. currentmodule:: mqt.qmap
+    .. autoclass:: TargetMetric
+
+
+The :code:`SynthesisConfiguration` class is used to provide several parameters to the :code:`synthesize_clifford` and the :code:`optimize_clifford` method. The following table lists the parameters and their default values.
+
+    .. currentmodule:: mqt.qmap
+    .. autoclass:: SynthesisConfiguration
+        :members:
diff --git a/docs/source/library/SynthesisResults.rst b/docs/source/library/SynthesisResults.rst
new file mode 100644
index 000000000..58ad79847
--- /dev/null
+++ b/docs/source/library/SynthesisResults.rst
@@ -0,0 +1,8 @@
+Synthesis Results
+=================
+
+This class captures additional results from the :func:`~mqt.qmap.synthesize_clifford` and the :func:`~mqt.qmap.optimize_clifford` method.
+
+    .. currentmodule:: mqt.qmap
+    .. autoclass:: SynthesisResults
+        :members:
diff --git a/docs/source/refs.bib b/docs/source/refs.bib
index 5059df2f2..7cf87affb 100644
--- a/docs/source/refs.bib
+++ b/docs/source/refs.bib
@@ -58,3 +58,11 @@ @inproceedings{peham2022OptimalSubarchitectures
   year = {2022},
   url = {https://arxiv.org/pdf/2210.09321.pdf},
 }
+
+@INPROCEEDINGS{schneider2023satEncodingOptimalClifford,
+  title = {A {SAT} Encoding for Optimal Clifford Circuit Synthesis},
+  booktitle = {Asia and South Pacific Design Automation Conference},
+  author = {Schneider, Sarah and Burgholzer, Lukas and Wille, Robert},
+  year = {2023},
+  url = {https://arxiv.org/pdf/2208.11713}
+}
diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp
new file mode 100644
index 000000000..b2e3a733a
--- /dev/null
+++ b/include/cliffordsynthesis/CliffordSynthesizer.hpp
@@ -0,0 +1,117 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#pragma once
+
+#include "QuantumComputation.hpp"
+#include "cliffordsynthesis/Configuration.hpp"
+#include "cliffordsynthesis/Results.hpp"
+#include "cliffordsynthesis/Tableau.hpp"
+#include "cliffordsynthesis/encoding/SATEncoder.hpp"
+
+#include <cstddef>
+#include <optional>
+#include <sstream>
+
+namespace cs {
+
+class CliffordSynthesizer {
+  using EncoderConfig = encoding::SATEncoder::Configuration;
+
+public:
+  CliffordSynthesizer() = default;
+  CliffordSynthesizer(Tableau initialTableau, Tableau targetTableau)
+      : initialTableau(std::move(initialTableau)),
+        targetTableau(std::move(targetTableau)) {}
+  explicit CliffordSynthesizer(Tableau targetTableau)
+      : initialTableau(targetTableau.getQubitCount()),
+        targetTableau(std::move(targetTableau)) {}
+  CliffordSynthesizer(Tableau initialTableau, qc::QuantumComputation& qc)
+      : initialTableau(std::move(initialTableau)), targetTableau(qc),
+        results(qc, targetTableau) {}
+  explicit CliffordSynthesizer(qc::QuantumComputation& qc)
+      : initialTableau(qc.getNqubits()), targetTableau(qc),
+        results(qc, targetTableau) {}
+
+  virtual ~CliffordSynthesizer() = default;
+
+  void synthesize(const Configuration& config = {});
+
+  [[nodiscard]] Results&                getResults() { return results; };
+  [[nodiscard]] qc::QuantumComputation& getResultCircuit() {
+    std::stringstream ss;
+    ss << results.getResultCircuit();
+    resultCircuit = std::make_unique<qc::QuantumComputation>();
+    resultCircuit->import(ss, qc::OpenQASM);
+    return *resultCircuit;
+  };
+  [[nodiscard]] Tableau& getResultTableau() {
+    std::stringstream ss;
+    ss << results.getResultTableau();
+    resultTableau.fromString(ss.str());
+    return resultTableau;
+  }
+
+protected:
+  Tableau initialTableau{};
+  Tableau targetTableau{};
+
+  Configuration configuration{};
+
+  Results                                 results{};
+  std::shared_ptr<qc::QuantumComputation> resultCircuit{};
+  Tableau                                 resultTableau{};
+  std::size_t                             solverCalls{};
+
+  static bool requiresMultiGateEncoding(const TargetMetric metric) {
+    return metric == TargetMetric::DEPTH;
+  }
+
+  void determineInitialTimestepLimit(EncoderConfig& config);
+  std::pair<std::size_t, std::size_t> determineUpperBound(EncoderConfig config);
+  void                                runMaxSAT(const EncoderConfig& config);
+  Results                             callSolver(const EncoderConfig& config);
+
+  void minimizeGatesFixedDepth(EncoderConfig config);
+
+  void gateOptimalSynthesis(EncoderConfig config, std::size_t lower,
+                            std::size_t upper);
+  void depthOptimalSynthesis(EncoderConfig config, std::size_t lower,
+                             std::size_t upper);
+  void twoQubitGateOptimalSynthesis(EncoderConfig config, std::size_t lower,
+                                    std::size_t upper);
+
+  void minimizeTwoQubitGatesFixedGateCount(std::size_t   gateCount,
+                                           EncoderConfig config);
+  void minimizeGatesFixedTwoQubitGateCount(EncoderConfig config);
+
+  template <typename T>
+  void runBinarySearch(T& value, T lowerBound, T upperBound,
+                       const EncoderConfig& config) {
+    INFO() << "Running binary search in range [" << lowerBound << ", "
+           << upperBound << ")";
+
+    while (lowerBound != upperBound) {
+      value = (lowerBound + upperBound) / 2;
+      INFO() << "Trying value " << value << " in range [" << lowerBound << ", "
+             << upperBound << ")";
+      const auto r = callSolver(config);
+      updateResults(configuration, r, results);
+      if (r.sat()) {
+        upperBound = value;
+        INFO() << "Found solution. New upper bound is " << upperBound;
+      } else {
+        lowerBound = value + 1;
+        INFO() << "No solution found. New lower bound is " << lowerBound;
+      }
+    }
+    INFO() << "Found optimum: " << lowerBound;
+  }
+
+  static void updateResults(const Configuration& config,
+                            const Results& newResults, Results& currentResults);
+};
+
+} // namespace cs
diff --git a/include/cliffordsynthesis/Configuration.hpp b/include/cliffordsynthesis/Configuration.hpp
new file mode 100644
index 000000000..6d97d89a9
--- /dev/null
+++ b/include/cliffordsynthesis/Configuration.hpp
@@ -0,0 +1,56 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#pragma once
+
+#include "TargetMetric.hpp"
+#include "nlohmann/json.hpp"
+
+namespace cs {
+struct Configuration {
+  Configuration() = default;
+
+  /// General configuration for the synthesis algorithm
+  std::size_t  initialTimestepLimit = 0U;
+  bool         useMaxSAT            = false;
+  TargetMetric target               = TargetMetric::GATES;
+  bool         useSymmetryBreaking  = true;
+
+  /// Settings for the SAT solver
+  std::size_t nThreads = 1U;
+
+  /// Settings for depth-optimal synthesis
+  bool minimizeGatesAfterDepthOptimization = false;
+
+  /// Settings for two-qubit gate-optimal synthesis
+  bool   tryHigherGateLimitForTwoQubitGateOptimization = false;
+  double gateLimitFactor                               = 1.1;
+  bool   minimizeGatesAfterTwoQubitGateOptimization    = false;
+
+  [[nodiscard]] nlohmann::json json() const {
+    nlohmann::json j;
+    j["initial_timestep_limit"] = initialTimestepLimit;
+    j["use_max_sat"]            = useMaxSAT;
+    j["target_metric"]          = toString(target);
+    j["use_symmetry_breaking"]  = useSymmetryBreaking;
+    j["n_threads"]              = nThreads;
+    j["minimize_gates_after_depth_optimization"] =
+        minimizeGatesAfterDepthOptimization;
+    j["try_higher_gate_limit_for_two_qubit_gate_optimization"] =
+        tryHigherGateLimitForTwoQubitGateOptimization;
+    j["gate_limit_factor"] = gateLimitFactor;
+    j["minimize_gates_after_two_qubit_gate_optimization"] =
+        minimizeGatesAfterTwoQubitGateOptimization;
+
+    return j;
+  }
+
+  friend std::ostream& operator<<(std::ostream&        os,
+                                  const Configuration& config) {
+    os << config.json().dump(2);
+    return os;
+  }
+};
+} // namespace cs
diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp
new file mode 100644
index 000000000..53f88f979
--- /dev/null
+++ b/include/cliffordsynthesis/Results.hpp
@@ -0,0 +1,106 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#pragma once
+
+#include "CircuitOptimizer.hpp"
+#include "LogicTerm/Logic.hpp"
+#include "cliffordsynthesis/Tableau.hpp"
+
+#include <nlohmann/json.hpp>
+#include <sstream>
+#include <string>
+
+namespace cs {
+class Results {
+public:
+  Results() = default;
+  Results(qc::QuantumComputation& qc, const Tableau& tableau) {
+    // SWAP gates are not natively supported in the encoding, so we need to
+    // decompose them into sequences of three CNOTs.
+    qc::CircuitOptimizer::decomposeSWAP(qc, false);
+
+    setResultCircuit(qc);
+    setResultTableau(tableau);
+    setDepth(qc.getDepth());
+    setSingleQubitGates(qc.getNsingleQubitOps());
+    setTwoQubitGates(qc.getNindividualOps() - singleQubitGates);
+    setSolverResult(logicbase::Result::SAT);
+  }
+
+  virtual ~Results() = default;
+
+  [[nodiscard]] std::size_t getGates() const {
+    return getSingleQubitGates() + getTwoQubitGates();
+  }
+  [[nodiscard]] std::size_t getTwoQubitGates() const { return twoQubitGates; }
+  [[nodiscard]] std::size_t getSingleQubitGates() const {
+    return singleQubitGates;
+  }
+  [[nodiscard]] std::size_t       getDepth() const { return depth; }
+  [[nodiscard]] double            getRuntime() const { return runtime; }
+  [[nodiscard]] logicbase::Result getSolverResult() const {
+    return solverResult;
+  }
+  [[nodiscard]] std::size_t getSolverCalls() const { return solverCalls; }
+
+  [[nodiscard]] std::string getResultCircuit() const { return resultCircuit; }
+  [[nodiscard]] std::string getResultTableau() const { return resultTableau; }
+
+  void setSingleQubitGates(const std::size_t g) { singleQubitGates = g; }
+  void setTwoQubitGates(const std::size_t g) { twoQubitGates = g; }
+  void setDepth(const std::size_t d) { depth = d; }
+  void setRuntime(const double t) { runtime = t; }
+  void setSolverResult(const logicbase::Result r) { solverResult = r; }
+  void setSolverCalls(const std::size_t c) { solverCalls = c; }
+
+  void setResultCircuit(qc::QuantumComputation& qc) {
+    std::stringstream ss;
+    qc.dumpOpenQASM(ss);
+    resultCircuit = ss.str();
+  }
+  void setResultTableau(const Tableau& tableau) {
+    std::stringstream ss;
+    ss << tableau;
+    resultTableau = ss.str();
+  }
+
+  [[nodiscard]] bool sat() const {
+    return getSolverResult() == logicbase::Result::SAT;
+  }
+  [[nodiscard]] bool unsat() const {
+    return getSolverResult() == logicbase::Result::UNSAT;
+  }
+
+  [[nodiscard]] virtual nlohmann::json json() const {
+    nlohmann::json resultJSON{};
+    resultJSON["solver_result"]      = toString(solverResult);
+    resultJSON["single_qubit_gates"] = singleQubitGates;
+    resultJSON["two_qubit_gates"]    = twoQubitGates;
+    resultJSON["depth"]              = depth;
+    resultJSON["runtime"]            = runtime;
+    resultJSON["solver_calls"]       = solverCalls;
+
+    return resultJSON;
+  }
+
+  friend std::ostream& operator<<(std::ostream& os, const Results& config) {
+    os << config.json().dump(2);
+    return os;
+  }
+
+protected:
+  logicbase::Result solverResult     = logicbase::Result::NDEF;
+  std::size_t       singleQubitGates = std::numeric_limits<std::size_t>::max();
+  std::size_t       twoQubitGates    = std::numeric_limits<std::size_t>::max();
+  std::size_t       depth            = std::numeric_limits<std::size_t>::max();
+  double            runtime          = 0.0;
+  std::size_t       solverCalls      = 0U;
+
+  std::string resultTableau{};
+  std::string resultCircuit{};
+};
+
+} // namespace cs
diff --git a/include/cliffordsynthesis/TargetMetric.hpp b/include/cliffordsynthesis/TargetMetric.hpp
new file mode 100644
index 000000000..69021d20e
--- /dev/null
+++ b/include/cliffordsynthesis/TargetMetric.hpp
@@ -0,0 +1,39 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#pragma once
+
+#include <iostream>
+#include <string>
+
+namespace cs {
+enum class TargetMetric { GATES, TWO_QUBIT_GATES, DEPTH };
+
+static std::string toString(const TargetMetric target) {
+  switch (target) {
+  case TargetMetric::GATES:
+    return "gates";
+  case TargetMetric::TWO_QUBIT_GATES:
+    return "two_qubit_gates";
+  case TargetMetric::DEPTH:
+    return "depth";
+  }
+  return "Error";
+}
+
+[[maybe_unused]] static TargetMetric
+targetMetricFromString(const std::string& target) {
+  if (target == "gates") {
+    return TargetMetric::GATES;
+  }
+  if (target == "two_qubit_gates") {
+    return TargetMetric::TWO_QUBIT_GATES;
+  }
+  if (target == "depth") {
+    return TargetMetric::DEPTH;
+  }
+  return TargetMetric::GATES;
+}
+} // namespace cs
diff --git a/include/cliffordsynthesis/encoding/GateEncoder.hpp b/include/cliffordsynthesis/encoding/GateEncoder.hpp
new file mode 100644
index 000000000..e8f1eb598
--- /dev/null
+++ b/include/cliffordsynthesis/encoding/GateEncoder.hpp
@@ -0,0 +1,120 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#pragma once
+
+#include "LogicBlock/LogicBlock.hpp"
+#include "cliffordsynthesis/Results.hpp"
+#include "cliffordsynthesis/encoding/TableauEncoder.hpp"
+#include "operations/OpType.hpp"
+
+#include <cstddef>
+#include <memory>
+
+namespace cs::encoding {
+
+class GateEncoder {
+public:
+  GateEncoder(const std::size_t nQubits, const std::size_t timestepLimit,
+              TableauEncoder::Variables*                    tvars,
+              const std::shared_ptr<logicbase::LogicBlock>& lb)
+      : N(nQubits), T(timestepLimit), tvars(tvars), lb(lb) {}
+  virtual ~GateEncoder() = default;
+
+  struct Variables {
+    // variables for the single-qubit gates
+    logicbase::LogicMatrix3D gS{};
+    // variables for the two-qubit gates
+    logicbase::LogicMatrix3D gC{};
+
+    void
+         collectSingleQubitGateVariables(std::size_t pos, std::size_t qubit,
+                                         logicbase::LogicVector& variables) const;
+    void collectTwoQubitGateVariables(std::size_t pos, std::size_t qubit,
+                                      bool                    target,
+                                      logicbase::LogicVector& variables) const;
+  };
+
+  // variable creation
+  void createSingleQubitGateVariables();
+  void createTwoQubitGateVariables();
+
+  // encode the relation between the tableaus and the gates
+  virtual void encodeGates() {
+    assertConsistency();
+    assertGateConstraints();
+  }
+
+  virtual void encodeSymmetryBreakingConstraints();
+
+  // extracting the circuit
+  void extractCircuitFromModel(Results& res, logicbase::Model& model);
+
+  [[nodiscard]] auto* getVariables() { return &vars; }
+
+  static constexpr std::array<qc::OpType, 7> SINGLE_QUBIT_GATES = {
+      qc::OpType::None, qc::OpType::X, qc::OpType::Y,   qc::OpType::Z,
+      qc::OpType::H,    qc::OpType::S, qc::OpType::Sdag};
+  [[nodiscard]] static constexpr std::size_t
+  gateToIndex(const qc::OpType type) {
+    for (std::size_t i = 0; i < SINGLE_QUBIT_GATES.size(); ++i) {
+      if (SINGLE_QUBIT_GATES[i] == type) {
+        return i;
+      }
+    }
+    return 0;
+  }
+
+protected:
+  // number of qubits N
+  std::size_t N{};
+  // timestep limit T
+  std::size_t T{};
+
+  // the gate variables
+  Variables vars{};
+
+  // the tableau variables
+  TableauEncoder::Variables* tvars{};
+
+  // the logic block to use
+  std::shared_ptr<logicbase::LogicBlock> lb{};
+
+  void assertExactlyOne(const logicbase::LogicVector& variables) const;
+
+  virtual void assertConsistency() const = 0;
+
+  virtual void assertGateConstraints()                           = 0;
+  virtual void assertSingleQubitGateConstraints(std::size_t pos) = 0;
+  [[nodiscard]] virtual logicbase::LogicTerm
+  createSingleQubitGateConstraint(std::size_t pos, std::size_t qubit,
+                                  qc::OpType gate)            = 0;
+  virtual void assertTwoQubitGateConstraints(std::size_t pos) = 0;
+  [[nodiscard]] virtual logicbase::LogicTerm
+  createTwoQubitGateConstraint(std::size_t pos, std::size_t ctrl,
+                               std::size_t trgt) = 0;
+
+  void extractSingleQubitGatesFromModel(std::size_t             pos,
+                                        logicbase::Model&       model,
+                                        qc::QuantumComputation& qc,
+                                        std::size_t& nSingleQubitGates);
+  void extractTwoQubitGatesFromModel(std::size_t pos, logicbase::Model& model,
+                                     qc::QuantumComputation& qc,
+                                     std::size_t&            nTwoQubitGates);
+
+  virtual void
+  assertSingleQubitGateSymmetryBreakingConstraints(std::size_t pos);
+  virtual void assertTwoQubitGateSymmetryBreakingConstraints(std::size_t pos);
+
+  virtual void assertSingleQubitGateOrderConstraints(std::size_t pos,
+                                                     std::size_t qubit) = 0;
+  virtual void assertSingleQubitGateCancellationConstraints(std::size_t pos,
+                                                            std::size_t qubit);
+
+  virtual void assertTwoQubitGateOrderConstraints(std::size_t pos,
+                                                  std::size_t ctrl,
+                                                  std::size_t trgt) = 0;
+};
+} // namespace cs::encoding
diff --git a/include/cliffordsynthesis/encoding/MultiGateEncoder.hpp b/include/cliffordsynthesis/encoding/MultiGateEncoder.hpp
new file mode 100644
index 000000000..26be2150b
--- /dev/null
+++ b/include/cliffordsynthesis/encoding/MultiGateEncoder.hpp
@@ -0,0 +1,39 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#pragma once
+
+#include "cliffordsynthesis/encoding/GateEncoder.hpp"
+
+#include <cstddef>
+#include <optional>
+
+namespace cs::encoding {
+
+class MultiGateEncoder : public GateEncoder {
+public:
+  using GateEncoder::GateEncoder;
+
+protected:
+  logicbase::LogicTerm rChanges{};
+
+  void assertConsistency() const override;
+  void assertGateConstraints() override;
+  void assertSingleQubitGateConstraints(std::size_t pos) override;
+  [[nodiscard]] logicbase::LogicTerm
+       createSingleQubitGateConstraint(std::size_t pos, std::size_t qubit,
+                                       qc::OpType gate) override;
+  void assertTwoQubitGateConstraints(std::size_t pos) override;
+  [[nodiscard]] logicbase::LogicTerm
+  createTwoQubitGateConstraint(std::size_t pos, std::size_t ctrl,
+                               std::size_t trgt) override;
+
+  void assertSingleQubitGateOrderConstraints(std::size_t pos,
+                                             std::size_t qubit) override;
+  void assertTwoQubitGateOrderConstraints(std::size_t pos, std::size_t ctrl,
+                                          std::size_t trgt) override;
+};
+
+} // namespace cs::encoding
diff --git a/include/cliffordsynthesis/encoding/ObjectiveEncoder.hpp b/include/cliffordsynthesis/encoding/ObjectiveEncoder.hpp
new file mode 100644
index 000000000..fb9364f18
--- /dev/null
+++ b/include/cliffordsynthesis/encoding/ObjectiveEncoder.hpp
@@ -0,0 +1,84 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#pragma once
+
+#include "cliffordsynthesis/TargetMetric.hpp"
+#include "cliffordsynthesis/encoding/GateEncoder.hpp"
+#include "cliffordsynthesis/encoding/TableauEncoder.hpp"
+
+#include <cstddef>
+#include <functional>
+#include <memory>
+
+namespace cs::encoding {
+
+class ObjectiveEncoder {
+public:
+  ObjectiveEncoder(const std::size_t nQubits, const std::size_t timestepLimit,
+                   GateEncoder::Variables*                       gvars,
+                   const std::shared_ptr<logicbase::LogicBlock>& lb)
+      : N(nQubits), T(timestepLimit), gvars(gvars), lb(lb) {}
+
+  template <class Op>
+  void limitGateCount(const std::size_t maxGateCount, Op op,
+                      const bool includeSingleQubitGates = true) const {
+    DEBUG() << "Limiting gate count to at most " << maxGateCount
+            << (includeSingleQubitGates ? "" : " two-qubit") << " gate(s)";
+
+    const auto cost = collectGateCount(includeSingleQubitGates);
+    lb->assertFormula(
+        op(cost, logicbase::LogicTerm(static_cast<int>(maxGateCount))));
+  }
+
+  void optimizeMetric(TargetMetric targetMetric) const;
+
+  void optimizeGateCount(bool includeSingleQubitGates = true) const;
+
+  void optimizeDepth(bool includeSingleQubitGates = true) const;
+
+protected:
+  // number of qubits N
+  std::size_t N{};
+  // timestep limit T
+  std::size_t T{};
+
+  // the gate variables
+  GateEncoder::Variables* gvars;
+
+  // the logic block
+  std::shared_ptr<logicbase::LogicBlock> lb;
+
+  [[nodiscard]] logicbase::LogicTerm
+  collectGateCount(bool includeSingleQubitGates = true) const;
+
+  template <class Op>
+  void collectSingleQubitGateTerms(std::size_t pos, logicbase::LogicTerm& terms,
+                                   Op op) const {
+    const auto& singleQubitGates = gvars->gS[pos];
+    for (std::size_t q = 0U; q < N; ++q) {
+      for (const auto gate : GateEncoder::SINGLE_QUBIT_GATES) {
+        if (gate == qc::OpType::None) {
+          continue;
+        }
+        terms = op(terms, singleQubitGates[GateEncoder::gateToIndex(gate)][q]);
+      }
+    }
+  }
+
+  template <class Op>
+  void collectTwoQubitGateTerms(std::size_t pos, logicbase::LogicTerm& terms,
+                                Op op) const {
+    const auto& twoQubitGates = gvars->gC[pos];
+    for (std::size_t ctrl = 0U; ctrl < N; ++ctrl) {
+      for (std::size_t trgt = 0U; trgt < ctrl; ++trgt) {
+        terms = op(terms, twoQubitGates[ctrl][trgt]);
+        terms = op(terms, twoQubitGates[trgt][ctrl]);
+      }
+    }
+  }
+};
+
+} // namespace cs::encoding
diff --git a/include/cliffordsynthesis/encoding/SATEncoder.hpp b/include/cliffordsynthesis/encoding/SATEncoder.hpp
new file mode 100644
index 000000000..557183ded
--- /dev/null
+++ b/include/cliffordsynthesis/encoding/SATEncoder.hpp
@@ -0,0 +1,89 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#pragma once
+
+#include "LogicBlock/LogicBlock.hpp"
+#include "cliffordsynthesis/Configuration.hpp"
+#include "cliffordsynthesis/Results.hpp"
+#include "cliffordsynthesis/Tableau.hpp"
+#include "cliffordsynthesis/encoding/GateEncoder.hpp"
+#include "cliffordsynthesis/encoding/ObjectiveEncoder.hpp"
+#include "cliffordsynthesis/encoding/TableauEncoder.hpp"
+#include "operations/OpType.hpp"
+
+#include <cstddef>
+#include <memory>
+#include <optional>
+
+namespace cs::encoding {
+
+class SATEncoder {
+public:
+  struct Configuration {
+    // the initial tableau to encode at t=0
+    Tableau* initialTableau{};
+
+    // the target tableau to encode at t=T
+    Tableau* targetTableau{};
+
+    // the number of qubits to encode
+    std::size_t nQubits{};
+
+    // the number of timesteps to encode
+    std::size_t timestepLimit{};
+
+    // the metric to optimize
+    TargetMetric targetMetric = TargetMetric::GATES;
+
+    // whether to use MaxSAT or Binary Search
+    bool useMaxSAT = false;
+
+    // whether to allow multiple gates per timestep
+    bool useMultiGateEncoding = false;
+
+    // whether to use symmetry breaking
+    bool useSymmetryBreaking = false;
+
+    // the number of threads to pass to the SAT solver
+    std::size_t nThreads = 1U;
+
+    // an optional limit on the total number of gates
+    std::optional<std::size_t> gateLimit = std::nullopt;
+
+    // an optional limit on the total number of two-qubit gates
+    std::optional<std::size_t> twoQubitGateLimit = std::nullopt;
+  };
+
+  SATEncoder() = default;
+  explicit SATEncoder(const Configuration& config)
+      : config(config), N(config.nQubits), T(config.timestepLimit) {}
+  virtual ~SATEncoder() = default;
+
+  virtual Results run();
+
+protected:
+  void                            initializeSolver();
+  void                            createFormulation();
+  void                            produceInstance() const;
+  [[nodiscard]] logicbase::Result solve() const;
+  void                            extractResultsFromModel(Results& res) const;
+  void                            cleanup() const;
+
+  std::shared_ptr<logicbase::LogicBlock> lb;
+  std::shared_ptr<TableauEncoder>        tableauEncoder;
+  std::shared_ptr<GateEncoder>           gateEncoder;
+  std::shared_ptr<ObjectiveEncoder>      objectiveEncoder;
+
+  // all configuration options for the encoder
+  Configuration config{};
+
+  // number of qubits N
+  std::size_t N{};
+  // timestep limit T
+  std::size_t T{};
+};
+
+} // namespace cs::encoding
diff --git a/include/cliffordsynthesis/encoding/SingleGateEncoder.hpp b/include/cliffordsynthesis/encoding/SingleGateEncoder.hpp
new file mode 100644
index 000000000..107a4a628
--- /dev/null
+++ b/include/cliffordsynthesis/encoding/SingleGateEncoder.hpp
@@ -0,0 +1,41 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#pragma once
+
+#include "cliffordsynthesis/encoding/GateEncoder.hpp"
+
+#include <cstddef>
+#include <optional>
+
+namespace cs::encoding {
+
+class SingleGateEncoder : public GateEncoder {
+public:
+  using GateEncoder::GateEncoder;
+
+protected:
+  void assertConsistency() const override;
+  void assertGateConstraints() override;
+  void assertSingleQubitGateConstraints(std::size_t pos) override;
+  [[nodiscard]] logicbase::LogicTerm
+       createSingleQubitGateConstraint(std::size_t pos, std::size_t qubit,
+                                       qc::OpType gate) override;
+  void assertTwoQubitGateConstraints(std::size_t pos) override;
+  [[nodiscard]] logicbase::LogicTerm
+  createTwoQubitGateConstraint(std::size_t pos, std::size_t ctrl,
+                               std::size_t trgt) override;
+
+  [[nodiscard]] logicbase::LogicTerm
+  createNoChange(std::size_t pos, std::size_t except,
+                 std::optional<std::size_t> except2) const;
+
+  void assertSingleQubitGateOrderConstraints(std::size_t pos,
+                                             std::size_t qubit) override;
+  void assertTwoQubitGateOrderConstraints(std::size_t pos, std::size_t ctrl,
+                                          std::size_t trgt) override;
+};
+
+} // namespace cs::encoding
diff --git a/include/cliffordsynthesis/encoding/TableauEncoder.hpp b/include/cliffordsynthesis/encoding/TableauEncoder.hpp
new file mode 100644
index 000000000..fea503716
--- /dev/null
+++ b/include/cliffordsynthesis/encoding/TableauEncoder.hpp
@@ -0,0 +1,76 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#pragma once
+
+#include "LogicBlock/LogicBlock.hpp"
+#include "cliffordsynthesis/Results.hpp"
+#include "cliffordsynthesis/Tableau.hpp"
+
+#include <cstddef>
+#include <memory>
+
+namespace cs::encoding {
+
+class TableauEncoder {
+public:
+  TableauEncoder() = default;
+  TableauEncoder(const std::size_t nQubits, const std::size_t timestepLimit,
+                 const std::shared_ptr<logicbase::LogicBlock>& lb)
+      : N(nQubits), T(timestepLimit), lb(lb) {}
+
+  struct Variables {
+    // variables for the X parts of the tableaus
+    logicbase::LogicMatrix x{};
+    // variables for the Z parts of the tableaus
+    logicbase::LogicMatrix z{};
+    // variables for the phase parts of the tableaus
+    logicbase::LogicVector r{};
+
+    // update rules for single-qubit gates
+    [[nodiscard]] logicbase::LogicTerm
+    singleQubitXChange(std::size_t pos, std::size_t qubit,
+                       qc::OpType gate) const;
+    [[nodiscard]] logicbase::LogicTerm
+    singleQubitZChange(std::size_t pos, std::size_t qubit,
+                       qc::OpType gate) const;
+    [[nodiscard]] logicbase::LogicTerm
+    singleQubitRChange(std::size_t pos, std::size_t qubit,
+                       qc::OpType gate) const;
+
+    // update rules for two-qubit gates
+    [[nodiscard]] std::pair<logicbase::LogicTerm, logicbase::LogicTerm>
+    twoQubitXChange(std::size_t pos, std::size_t ctrl, std::size_t trgt) const;
+    [[nodiscard]] std::pair<logicbase::LogicTerm, logicbase::LogicTerm>
+    twoQubitZChange(std::size_t pos, std::size_t ctrl, std::size_t trgt) const;
+    [[nodiscard]] logicbase::LogicTerm
+    twoQubitRChange(std::size_t pos, std::size_t ctrl, std::size_t trgt) const;
+  };
+
+  // variable creation
+  void createTableauVariables();
+
+  // fixing the tableau
+  void assertTableau(const Tableau& tableau, std::size_t t);
+
+  // extracting the tableau
+  void extractTableauFromModel(Results& results, std::size_t t,
+                               logicbase::Model& model) const;
+
+  [[nodiscard]] auto* getVariables() { return &vars; }
+
+protected:
+  // number of qubits N
+  std::size_t N{};
+  // timestep limit T
+  std::size_t T{};
+
+  // the tableau variables
+  Variables vars{};
+
+  // the logic block to use
+  std::shared_ptr<logicbase::LogicBlock> lb{};
+};
+} // namespace cs::encoding
diff --git a/mqt/qmap/CMakeLists.txt b/mqt/qmap/CMakeLists.txt
index 674575f75..4ccdc1b40 100644
--- a/mqt/qmap/CMakeLists.txt
+++ b/mqt/qmap/CMakeLists.txt
@@ -3,4 +3,5 @@ target_link_libraries(py${PROJECT_NAME} PUBLIC ${PROJECT_NAME}_heuristic_lib MQT
                                                pybind11_json)
 target_compile_definitions(py${PROJECT_NAME} PUBLIC Z3_FOUND)
 target_link_libraries(py${PROJECT_NAME} PUBLIC ${PROJECT_NAME}_exact_lib)
+target_link_libraries(py${PROJECT_NAME} PUBLIC ${PROJECT_NAME}_cliffordsynthesis_lib)
 target_compile_definitions(py${PROJECT_NAME} PRIVATE VERSION_INFO=${QMAP_VERSION_INFO})
diff --git a/mqt/qmap/__init__.py b/mqt/qmap/__init__.py
index 506fa0b59..887a2d7d6 100644
--- a/mqt/qmap/__init__.py
+++ b/mqt/qmap/__init__.py
@@ -15,10 +15,12 @@
     if bin_path.exists():
         os.add_dll_directory(str(bin_path))
 
+from mqt.qmap.clifford_synthesis import optimize_clifford, synthesize_clifford
 from mqt.qmap.compile import compile
 from mqt.qmap.pyqmap import (
     Arch,
     Architecture,
+    CliffordSynthesizer,
     CommanderGrouping,
     Configuration,
     Encoding,
@@ -26,7 +28,12 @@
     Layering,
     MappingResults,
     Method,
+    QuantumComputation,
     SwapReduction,
+    SynthesisConfiguration,
+    SynthesisResults,
+    Tableau,
+    TargetMetric,
 )
 from mqt.qmap.subarchitectures import SubarchitectureOrder
 
@@ -43,4 +50,12 @@
     "MappingResults",
     "Architecture",
     "SubarchitectureOrder",
+    "SynthesisConfiguration",
+    "SynthesisResults",
+    "TargetMetric",
+    "QuantumComputation",
+    "Tableau",
+    "CliffordSynthesizer",
+    "synthesize_clifford",
+    "optimize_clifford",
 ]
diff --git a/mqt/qmap/bindings.cpp b/mqt/qmap/bindings.cpp
index 37a36cb3e..10873a7e4 100644
--- a/mqt/qmap/bindings.cpp
+++ b/mqt/qmap/bindings.cpp
@@ -3,6 +3,7 @@
 // See README.md or go to https://github.com/cda-tum/qmap for more information.
 //
 
+#include "cliffordsynthesis/CliffordSynthesizer.hpp"
 #include "exact/ExactMapper.hpp"
 #include "heuristic/HeuristicMapper.hpp"
 #include "nlohmann/json.hpp"
@@ -369,6 +370,170 @@ PYBIND11_MODULE(pyqmap, m) {
 
   // Main mapping function
   m.def("map", &map, "map a quantum circuit");
+
+  // Target metric for the Clifford synthesizer
+  py::enum_<cs::TargetMetric>(m, "TargetMetric")
+      .value("gates", cs::TargetMetric::GATES, "Optimize gate count.")
+      .value("two_qubit_gates", cs::TargetMetric::TWO_QUBIT_GATES,
+             "Optimize two-qubit gate count.")
+      .value("depth", cs::TargetMetric::DEPTH, "Optimize circuit depth.")
+      .export_values()
+      .def(py::init([](const std::string& name) {
+        return cs::targetMetricFromString(name);
+      }));
+  py::implicitly_convertible<py::str, cs::TargetMetric>();
+
+  // Configuration for the synthesis
+  py::class_<cs::Configuration>(
+      m, "SynthesisConfiguration",
+      "Configuration options for the MQT QMAP Clifford synthesis tool.")
+      .def(py::init<>())
+      .def_readwrite("initial_timestep_limit",
+                     &cs::Configuration::initialTimestepLimit,
+                     "Initial timestep limit for the Clifford synthesis. "
+                     "Defaults to `0`, which implies that the initial timestep "
+                     "limit is determined automatically.")
+      .def_readwrite(
+          "use_maxsat", &cs::Configuration::useMaxSAT,
+          "Use MaxSAT to solve the synthesis problem or to really on the "
+          "binary search scheme for finding the optimum. Defaults to `false`.")
+      .def_readwrite(
+          "target_metric", &cs::Configuration::target,
+          "Target metric for the Clifford synthesis. Defaults to `gates`.")
+      .def_readwrite("use_symmetry_breaking",
+                     &cs::Configuration::useSymmetryBreaking,
+                     "Use symmetry breaking clauses to speed up the synthesis "
+                     "process. Defaults to `true`.")
+      .def_readwrite(
+          "n_threads", &cs::Configuration::nThreads,
+          "Number of threads to use for the synthesis. Defaults to `1`.")
+      .def_readwrite(
+          "minimize_gates_after_depth_optimization",
+          &cs::Configuration::minimizeGatesAfterDepthOptimization,
+          "Depth optimization might produce a circuit with more gates than "
+          "necessary. This option enables an additional run of the synthesizer "
+          "to minimize the overall number of gates. Defaults to `false`.")
+      .def_readwrite(
+          "try_higher_gate_limit_for_two_qubit_gate_optimization",
+          &cs::Configuration::tryHigherGateLimitForTwoQubitGateOptimization,
+          "When optimizing two-qubit gates, the synthesizer might fail "
+          "to find an optimal solution for a certain timestep limit, but there "
+          "might be a better solution for some higher timestep limit. This "
+          "option enables an additional run of the synthesizer with a higher "
+          "gate limit. Defaults to `false`.")
+      .def_readwrite("gate_limit_factor", &cs::Configuration::gateLimitFactor,
+                     "Factor by which the gate limit is increased when "
+                     "trying to find a better solution for the two-qubit "
+                     "gate optimization. Defaults to `1.1`.")
+      .def_readwrite(
+          "minimize_gates_after_two_qubit_gate_optimization",
+          &cs::Configuration::minimizeGatesAfterTwoQubitGateOptimization,
+          "Two-qubit gate optimization might produce a circuit "
+          "with more gates than necessary. This option enables "
+          "an additional run of the synthesizer to minimize the "
+          "overall number of gates. Defaults to `false`.")
+      .def("json", &cs::Configuration::json,
+           "Returns a JSON-style dictionary of all the information present in "
+           "the :class:`.Configuration`")
+      .def(
+          "__repr__",
+          [](const cs::Configuration& config) { return config.json().dump(2); },
+          "Prints a JSON-formatted representation of all the information "
+          "present in the :class:`.Configuration`");
+
+  // Results of the synthesis
+  py::class_<cs::Results>(m, "SynthesisResults",
+                          "Results of the MQT QMAP Clifford synthesis tool.")
+      .def(py::init<>())
+      .def_property_readonly("gates", &cs::Results::getGates,
+                             "Returns the number of gates in the circuit.")
+      .def_property_readonly("single_qubit_gates",
+                             &cs::Results::getSingleQubitGates,
+                             "Returns the number of single-qubit gates in the "
+                             "synthesized circuit.")
+      .def_property_readonly("two_qubit_gates", &cs::Results::getTwoQubitGates,
+                             "Returns the number of two-qubit gates in the "
+                             "synthesized circuit.")
+      .def_property_readonly("depth", &cs::Results::getDepth,
+                             "Returns the depth of the synthesized circuit.")
+      .def_property_readonly("runtime", &cs::Results::getRuntime,
+                             "Returns the runtime of the synthesis in seconds.")
+      .def_property_readonly("solver_calls", &cs::Results::getSolverCalls,
+                             "Returns the number of calls to the SAT solver.")
+      .def_property_readonly(
+          "circuit", &cs::Results::getResultCircuit,
+          "Returns the synthesized circuit as a qasm string.")
+      .def_property_readonly("tableau", &cs::Results::getResultTableau,
+                             "Returns a string representation of the "
+                             "synthesized circuit's tableau.")
+      .def("sat", &cs::Results::sat,
+           "Returns `true` if the synthesis was successful.")
+      .def("unsat", &cs::Results::unsat,
+           "Returns `true` if the synthesis was unsuccessful.");
+
+  auto tableau = py::class_<cs::Tableau>(
+      m, "Tableau", "A class for representing stabilizer tableaus.");
+  tableau.def(py::init<std::size_t>(), "n"_a,
+              "Creates a tableau for an n-qubit Clifford.");
+  tableau.def(
+      py::init<const std::string&>(), "tableau"_a,
+      "Constructs a tableau from a string description. This can either be a "
+      "semicolon separated binary matrix or a list of Pauli strings.");
+
+  auto quantumComputation = py::class_<qc::QuantumComputation>(
+      m, "QuantumComputation",
+      "A class for the intermediate representation of quantum circuits in the "
+      "Munich Quantum Toolkit.");
+  quantumComputation.def_static(
+      "from_file",
+      [](const std::string& filename) {
+        return qc::QuantumComputation(filename);
+      },
+      "filename"_a, "Reads a quantum circuit from a file.");
+  quantumComputation.def_static(
+      "from_qasm_str",
+      [](const std::string& qasm) {
+        std::stringstream      ss(qasm);
+        qc::QuantumComputation qc{};
+        qc.import(ss, qc::Format::OpenQASM);
+        return qc;
+      },
+      "qasm"_a, "Reads a quantum circuit from a qasm string.");
+  quantumComputation.def_static(
+      "from_qiskit",
+      [](const py::object& circuit) {
+        qc::QuantumComputation qc{};
+        qc::qiskit::QuantumCircuit::import(qc, circuit);
+        return qc;
+      },
+      "circuit"_a,
+      "Reads a quantum circuit from a Qiskit :class:`QuantumCircuit`.");
+
+  auto synthesizer = py::class_<cs::CliffordSynthesizer>(
+      m, "CliffordSynthesizer", "A class for synthesizing Clifford circuits.");
+
+  synthesizer.def(py::init<cs::Tableau, cs::Tableau>(), "initial_tableau"_a,
+                  "target_tableau"_a,
+                  "Constructs a synthesizer for two tableaus representing the "
+                  "initial and target state.");
+  synthesizer.def(py::init<cs::Tableau>(), "target_tableau"_a,
+                  "Constructs a synthesizer for a tableau representing the "
+                  "target state.");
+  synthesizer.def(py::init<qc::QuantumComputation&>(), "qc"_a,
+                  "Constructs a synthesizer for a quantum computation "
+                  "representing the target state.");
+  synthesizer.def(
+      py::init<cs::Tableau, qc::QuantumComputation&>(), "initial_tableau"_a,
+      "qc"_a,
+      "Constructs a synthesizer for a quantum computation representing the "
+      "target state that starts in an initial state represented by a tableau.");
+  synthesizer.def("synthesize", &cs::CliffordSynthesizer::synthesize,
+                  "config"_a = cs::Configuration(),
+                  "Runs the synthesis with the given configuration.");
+  synthesizer.def_property_readonly("results",
+                                    &cs::CliffordSynthesizer::getResults,
+                                    "Returns the results of the synthesis.");
+
 #ifdef VERSION_INFO
   m.attr("__version__") = MACRO_STRINGIFY(VERSION_INFO);
 #else
diff --git a/mqt/qmap/clifford_synthesis.py b/mqt/qmap/clifford_synthesis.py
new file mode 100644
index 000000000..24c3fadf2
--- /dev/null
+++ b/mqt/qmap/clifford_synthesis.py
@@ -0,0 +1,151 @@
+#
+# This file is part of MQT QMAP library which is released under the MIT license.
+# See file README.md or go to http://iic.jku.at/eda/research/quantum_verification/ for more information.
+#
+from __future__ import annotations
+
+from typing import Any
+
+from qiskit import QuantumCircuit
+from qiskit.quantum_info import Clifford, PauliList
+
+from .compile import extract_initial_layout_from_qasm
+from .pyqmap import (
+    CliffordSynthesizer,
+    QuantumComputation,
+    SynthesisConfiguration,
+    SynthesisResults,
+    Tableau,
+)
+
+
+def _import_circuit(circuit: str | QuantumCircuit | QuantumComputation) -> QuantumComputation:
+    """Import a circuit from a string, a QuantumCircuit, or a QuantumComputation."""
+    if isinstance(circuit, QuantumCircuit):
+        return QuantumComputation.from_qiskit(circuit)
+    elif isinstance(circuit, str):
+        if circuit.endswith(".qasm"):
+            return QuantumComputation.from_file(circuit)
+        else:
+            return QuantumComputation.from_qasm_str(circuit)
+    else:
+        return circuit
+
+
+def _import_tableau(tableau: str | Clifford | PauliList | Tableau) -> Tableau:
+    """Import a tableau from a string, a Clifford, a PauliList, or a Tableau."""
+    if isinstance(tableau, Clifford):
+        try:
+            return Tableau(str(tableau.to_labels(mode="S")))
+        except AttributeError:
+            return Tableau(str(tableau.stabilizer.to_labels()))
+    elif isinstance(tableau, PauliList):
+        return Tableau(str(tableau.to_labels()))
+    elif isinstance(tableau, str):
+        return Tableau(tableau)
+    else:
+        return tableau
+
+
+def _config_from_kwargs(kwargs: dict[str, Any]) -> SynthesisConfiguration:
+    """Creates a :class:`SynthesisConfiguration` from keyword arguments."""
+    config = SynthesisConfiguration()
+    for key, value in kwargs.items():
+        if hasattr(config, key):
+            setattr(config, key, value)
+        else:
+            raise ValueError(f"Invalid keyword argument: {key}")
+    return config
+
+
+def _circuit_from_qasm(qasm: str) -> QuantumCircuit:
+    """Creates a proper :class:`qiskit.QuantumCircuit` from a QASM string (including layout information)."""
+    circ = QuantumCircuit.from_qasm_str(qasm)
+    layout = extract_initial_layout_from_qasm(qasm, circ.qregs)
+
+    # qiskit-terra 0.22.0 introduced a breaking change in the `_layout` of the `QuantumCircuit` class.
+    # To maintain backwards compatibility, the following `try... except` block is necessary.
+    try:
+        from qiskit.transpiler.layout import TranspileLayout
+
+        circ._layout = TranspileLayout(initial_layout=layout, input_qubit_mapping=layout.get_virtual_bits())
+    except ImportError:
+        circ._layout = layout
+
+    return circ
+
+
+def synthesize_clifford(
+    target_tableau: str | Clifford | PauliList | Tableau,
+    initial_tableau: str | Clifford | PauliList | Tableau = None,
+    **kwargs: Any,
+) -> tuple[QuantumCircuit, SynthesisResults]:
+    """Synthesize a Clifford circuit from a given tableau starting from an (optional) initial tableau.
+
+    target_tableau: str | Clifford | PauliList | Tableau
+        The target tableau to synthesize.
+        If a string is given, it is interpreted as a semicolon separated binary matrix or a list of Pauli strings.
+        If a :class:`Clifford` or a :class:`PauliList` is given, it is converted to a :class:`Tableau`.
+        If a :class:`Tableau` is given, it is used directly.
+    initial_tableau: str | Clifford | PauliList | Tableau | None
+        The initial tableau to start from.
+        If a string is given, it is interpreted as a semicolon separated binary matrix or a list of Pauli strings.
+        If a :class:`Clifford` or a :class:`PauliList` is given, it is converted to a :class:`Tableau`.
+        If a :class:`Tableau` is given, it is used directly.
+        If no initial tableau is given, the synthesis starts from the identity tableau.
+    kwargs: dict[str, Any]
+        Additional keyword arguments to configure the synthesis.
+        See :class:`SynthesisConfiguration` for a list of available options.
+    """
+    config = _config_from_kwargs(kwargs)
+
+    tableau = _import_tableau(target_tableau)
+    if initial_tableau is not None:
+        synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau), tableau)
+    else:
+        synthesizer = CliffordSynthesizer(tableau)
+
+    synthesizer.synthesize(config)
+
+    results = synthesizer.results
+    circ = _circuit_from_qasm(results.circuit)
+
+    return circ, results
+
+
+def optimize_clifford(
+    circuit: str | QuantumCircuit | QuantumComputation,
+    initial_tableau: str | Clifford | PauliList | Tableau = None,
+    **kwargs: Any,
+) -> tuple[QuantumCircuit, SynthesisResults]:
+    """Optimize a Clifford circuit starting from an (optional) initial tableau.
+
+    circuit: str | QuantumCircuit | QuantumComputation | None
+        The circuit to optimize.
+        If a string is given, it is interpreted as a QASM string or a filename.
+        If a :class:`QuantumCircuit` is given, it is converted to a :class:`QuantumComputation`.
+        If a :class:`QuantumComputation` is given, it is used as is.
+    initial_tableau: str | Clifford | PauliList | Tableau | None
+        The initial tableau to start from.
+        If a string is given, it is interpreted as a semicolon separated binary matrix or a list of Pauli strings.
+        If a :class:`Clifford` is given or a :class:`PauliList` is given, it is converted to a Tableau.
+        If a :class:`Tableau` is given, it is used directly.
+        If no initial tableau is given, the synthesis starts from the identity tableau.
+    kwargs: dict[str, Any]
+        Additional keyword arguments to configure the synthesis.
+        See :class:`SynthesisConfiguration` for a list of available options.
+    """
+    config = _config_from_kwargs(kwargs)
+
+    qc = _import_circuit(circuit)
+    if initial_tableau is not None:
+        synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau), qc)
+    else:
+        synthesizer = CliffordSynthesizer(qc)
+
+    synthesizer.synthesize(config)
+
+    results = synthesizer.results
+    circ = _circuit_from_qasm(results.circuit)
+
+    return circ, results
diff --git a/mqt/qmap/pyqmap.pyi b/mqt/qmap/pyqmap.pyi
index dcdbc1800..644414086 100644
--- a/mqt/qmap/pyqmap.pyi
+++ b/mqt/qmap/pyqmap.pyi
@@ -2,6 +2,8 @@ from __future__ import annotations
 
 from typing import Any, ClassVar, overload
 
+from qiskit import QuantumCircuit
+
 class Arch:
     __members__: ClassVar[dict[Arch, int]] = ...  # read-only
     IBMQ_Bogota: ClassVar[Arch] = ...
@@ -265,3 +267,88 @@ class SwapReduction:
     def value(self) -> int: ...
 
 def map(arg0: object, arg1: Architecture, arg2: Configuration) -> MappingResults: ...
+
+class TargetMetric:
+    __members__: ClassVar[dict[TargetMetric, int]] = ...  # read-only
+    depth: ClassVar[TargetMetric] = ...
+    gates: ClassVar[TargetMetric] = ...
+    two_qubit_gates: ClassVar[TargetMetric] = ...
+    @overload
+    def __init__(self, value: int) -> None: ...
+    @overload
+    def __init__(self, arg0: str) -> None: ...
+    @overload
+    def __init__(self, arg0: TargetMetric) -> None: ...
+    def __eq__(self, other: object) -> bool: ...
+    def __getstate__(self) -> int: ...
+    def __hash__(self) -> int: ...
+    def __index__(self) -> int: ...
+    def __int__(self) -> int: ...
+    def __ne__(self, other: object) -> bool: ...
+    def __setstate__(self, state: int) -> None: ...
+    @property
+    def name(self) -> str: ...
+    @property
+    def value(self) -> int: ...
+
+class SynthesisConfiguration:
+    gate_limit_factor: float
+    initial_timestep_limit: int
+    minimize_gates_after_depth_optimization: bool
+    minimize_gates_after_two_qubit_gate_optimization: bool
+    n_threads: int
+    target_metric: TargetMetric
+    try_higher_gate_limit_for_two_qubit_gate_optimization: bool
+    use_maxsat: bool
+    use_symmetry_breaking: bool
+    def __init__(self) -> None: ...
+    def json(self) -> dict[str, Any]: ...
+
+class SynthesisResults:
+    def __init__(self) -> None: ...
+    def sat(self) -> bool: ...
+    def unsat(self) -> bool: ...
+    @property
+    def circuit(self) -> str: ...
+    @property
+    def depth(self) -> int: ...
+    @property
+    def gates(self) -> int: ...
+    @property
+    def runtime(self) -> float: ...
+    @property
+    def single_qubit_gates(self) -> int: ...
+    @property
+    def solver_calls(self) -> int: ...
+    @property
+    def tableau(self) -> str: ...
+    @property
+    def two_qubit_gates(self) -> int: ...
+
+class QuantumComputation:
+    def __init__(self) -> None: ...
+    @staticmethod
+    def from_file(file: str) -> QuantumComputation: ...
+    @staticmethod
+    def from_qasm_str(qasm: str) -> QuantumComputation: ...
+    @staticmethod
+    def from_qiskit(circuit: QuantumCircuit) -> QuantumComputation: ...
+
+class Tableau:
+    @overload
+    def __init__(self, n: int) -> None: ...
+    @overload
+    def __init__(self, description: str) -> None: ...
+
+class CliffordSynthesizer:
+    @overload
+    def __init__(self, initial_tableau: Tableau, target_tableau: Tableau) -> None: ...
+    @overload
+    def __init__(self, target_tableau: Tableau) -> None: ...
+    @overload
+    def __init__(self, qc: QuantumComputation) -> None: ...
+    @overload
+    def __init__(self, initial_tableau: Tableau, qc: QuantumComputation) -> None: ...
+    def synthesize(self, config: SynthesisConfiguration = ...) -> None: ...
+    @property
+    def results(self) -> SynthesisResults: ...
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e145746dc..924452610 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -29,7 +29,7 @@ macro(ADD_INTERNAL_LIBRARY libname srcfile)
   if(MSVC)
     target_compile_options(${lib} PUBLIC /utf-8)
   else()
-    target_compile_options(${lib} PUBLIC -Wall -Wextra $<$<CONFIG:DEBUG>:-g3>)
+    target_compile_options(${lib} PUBLIC -Wall -Wextra $<$<CONFIG:DEBUG>:-g3 -ggdb>)
     if(BINDINGS)
       # adjust visibility settings for building Python bindings
       target_compile_options(${lib} PUBLIC -fvisibility=hidden)
@@ -90,12 +90,26 @@ macro(ADD_SYNTHESIS_LIBRARY libname srcfile)
   add_library(
     ${lib}
     ${CMAKE_CURRENT_SOURCE_DIR}/utils.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/Architecture.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/cliffordsynthesis/encoding/SATEncoder.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/cliffordsynthesis/encoding/TableauEncoder.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/cliffordsynthesis/encoding/GateEncoder.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/cliffordsynthesis/encoding/SingleGateEncoder.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/cliffordsynthesis/encoding/MultiGateEncoder.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/cliffordsynthesis/encoding/ObjectiveEncoder.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/cliffordsynthesis/Tableau.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/${libname}/${srcfile}.cpp
     ${${PROJECT_NAME}_SOURCE_DIR}/include/utils.hpp
-    ${${PROJECT_NAME}_SOURCE_DIR}/include/Architecture.hpp
+    ${${PROJECT_NAME}_SOURCE_DIR}/include/cliffordsynthesis/Configuration.hpp
+    ${${PROJECT_NAME}_SOURCE_DIR}/include/cliffordsynthesis/Results.hpp
+    ${${PROJECT_NAME}_SOURCE_DIR}/include/cliffordsynthesis/encoding/SATEncoder.hpp
+    ${${PROJECT_NAME}_SOURCE_DIR}/include/cliffordsynthesis/encoding/TableauEncoder.hpp
+    ${${PROJECT_NAME}_SOURCE_DIR}/include/cliffordsynthesis/encoding/GateEncoder.hpp
+    ${${PROJECT_NAME}_SOURCE_DIR}/include/cliffordsynthesis/encoding/SingleGateEncoder.hpp
+    ${${PROJECT_NAME}_SOURCE_DIR}/include/cliffordsynthesis/encoding/MultiGateEncoder.hpp
+    ${${PROJECT_NAME}_SOURCE_DIR}/include/cliffordsynthesis/encoding/ObjectiveEncoder.hpp
     ${${PROJECT_NAME}_SOURCE_DIR}/include/cliffordsynthesis/Tableau.hpp
-    ${${PROJECT_NAME}_SOURCE_DIR}/include/configuration/AvailableArchitecture.hpp)
+    ${${PROJECT_NAME}_SOURCE_DIR}/include/cliffordsynthesis/TargetMetric.hpp
+    ${${PROJECT_NAME}_SOURCE_DIR}/include/${libname}/${srcfile}.hpp)
 
   add_internal_library(${lib} ${srcfile})
 endmacro()
diff --git a/src/cliffordsynthesis/CliffordSynthesizer.cpp b/src/cliffordsynthesis/CliffordSynthesizer.cpp
new file mode 100644
index 000000000..c6c679976
--- /dev/null
+++ b/src/cliffordsynthesis/CliffordSynthesizer.cpp
@@ -0,0 +1,376 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#include "cliffordsynthesis/CliffordSynthesizer.hpp"
+
+#include "LogicTerm/Logic.hpp"
+#include "utils/logging.hpp"
+
+#include <chrono>
+
+namespace cs {
+
+void CliffordSynthesizer::synthesize(const Configuration& config) {
+  configuration = config;
+
+  INFO() << "Optimization target: " << toString(configuration.target);
+
+  const auto start = std::chrono::high_resolution_clock::now();
+
+  // create the general configuration for the SAT encoder
+  auto encoderConfig                = EncoderConfig();
+  encoderConfig.initialTableau      = &initialTableau;
+  encoderConfig.targetTableau       = &targetTableau;
+  encoderConfig.nQubits             = initialTableau.getQubitCount();
+  encoderConfig.timestepLimit       = configuration.initialTimestepLimit;
+  encoderConfig.targetMetric        = configuration.target;
+  encoderConfig.useMaxSAT           = configuration.useMaxSAT;
+  encoderConfig.useSymmetryBreaking = configuration.useSymmetryBreaking;
+  encoderConfig.nThreads            = configuration.nThreads;
+  encoderConfig.useMultiGateEncoding =
+      requiresMultiGateEncoding(encoderConfig.targetMetric);
+
+  // First, determine an initial guess for the number of timesteps. This can
+  // either be specified as a configuration parameter or starts at 1.
+  determineInitialTimestepLimit(encoderConfig);
+
+  // Then, determine an upper bound for the number of timesteps by solving the
+  // SAT problem repeatedly with increasing timestep limits until a satisfying
+  // assignment is found. This uses the general SAT encoding without any
+  // objective function regardless of the configuration.
+  const auto [lower, upper] = determineUpperBound(encoderConfig);
+
+  // if the upper bound is 0, the solution does not require any gates and the
+  // synthesis is done.
+  if (upper == 0U) {
+    INFO() << "No gates required.";
+    return;
+  }
+  // Otherwise, the determined upper bound is used as an initial timestep limit.
+  encoderConfig.timestepLimit = upper;
+
+  // Once a valid upper bound is found, the SAT problem is solved again with
+  // the objective function encoded.
+  switch (config.target) {
+  case TargetMetric::GATES:
+    gateOptimalSynthesis(encoderConfig, lower, upper);
+    break;
+  case TargetMetric::DEPTH:
+    depthOptimalSynthesis(encoderConfig, lower, upper);
+    break;
+  case TargetMetric::TWO_QUBIT_GATES:
+    twoQubitGateOptimalSynthesis(encoderConfig, 0U, results.getTwoQubitGates());
+    break;
+  }
+
+  results.setSolverCalls(solverCalls);
+
+  const auto end = std::chrono::high_resolution_clock::now();
+  const std::chrono::duration<double> diff = end - start;
+  INFO() << "Synthesis took " << diff.count() << " seconds";
+  results.setRuntime(diff.count());
+}
+
+void CliffordSynthesizer::determineInitialTimestepLimit(EncoderConfig& config) {
+  if (config.timestepLimit != 0U) {
+    INFO() << "Using configured initial timestep limit: "
+           << config.timestepLimit;
+    return;
+  }
+
+  // in case no circuit was provided as input, the best guess is to start low
+  // and increase the limit geometrically until a solution is found.
+  if (!results.sat()) {
+    config.timestepLimit = 1U;
+    INFO()
+        << "No initial circuit specified. Using initial timestep limit of 1.";
+    return;
+  }
+
+  // If an initial circuit is specified, there already is a satisfying result.
+  // We can use its gates or depth as a starting point for the number of
+  // timesteps. Furthermore, no upper bound needs to be determined.
+  if (requiresMultiGateEncoding(config.targetMetric)) {
+    config.timestepLimit = results.getDepth();
+    INFO() << "Using initial circuit's depth as initial timestep limit: "
+           << config.timestepLimit;
+  } else {
+    config.timestepLimit = results.getGates();
+    INFO() << "Using initial circuit's gate count as initial timestep limit: "
+           << config.timestepLimit;
+  }
+}
+
+std::pair<std::size_t, std::size_t>
+CliffordSynthesizer::determineUpperBound(EncoderConfig config) {
+  // In case the synthesis was started with a circuit, the upper bound is
+  // inherently given by the circuit and does not need to be computed here.
+  if (results.sat()) {
+    return {0U, config.timestepLimit};
+  }
+
+  std::size_t lowerBound = 0U;
+  std::size_t upperBound = config.timestepLimit;
+
+  INFO() << "Searching for upper bound for the number of timesteps starting "
+         << "with " << upperBound;
+
+  config.useMaxSAT = false;
+  while (!results.sat()) {
+    results = callSolver(config);
+    if (!results.sat()) {
+      lowerBound = upperBound + 1U;
+      upperBound *= 2U;
+      INFO() << "No solution found for " << config.timestepLimit
+             << " timestep(s). Doubling timestep limit to " << upperBound;
+      config.timestepLimit = upperBound;
+    }
+  }
+
+  if (config.targetMetric == TargetMetric::GATES ||
+      config.targetMetric == TargetMetric::TWO_QUBIT_GATES) {
+    upperBound = std::min(upperBound, results.getGates());
+  } else if (config.targetMetric == TargetMetric::DEPTH) {
+    upperBound = std::min(upperBound, results.getDepth());
+  }
+
+  INFO() << "Found upper bound for the number of timesteps: " << upperBound;
+  return {lowerBound, upperBound};
+}
+
+void CliffordSynthesizer::gateOptimalSynthesis(EncoderConfig     config,
+                                               const std::size_t lower,
+                                               const std::size_t upper) {
+  // Gate-optimal synthesis is achieved by determining a timestep limit T such
+  // that there exists a solution with T gates, but no solution with T-1 gates.
+  // This procedure uses an encoding where a single gate is allowed per timestep
+  // and guarantees optimality, i.e., there is no solution with fewer gates.
+
+  if (configuration.useMaxSAT) {
+    // The MaxSAT solver can determine the optimal T with a single call by
+    // minimizing over the number of applied gates.
+    runMaxSAT(config);
+  } else {
+    // The binary search approach calls the SAT solver repeatedly with varying
+    // timestep (=gate) limits T until a solution with T gates is found, but no
+    // solution with T-1 gates could be determined.
+    runBinarySearch(config.timestepLimit, lower, upper, config);
+  }
+}
+
+void CliffordSynthesizer::depthOptimalSynthesis(
+    CliffordSynthesizer::EncoderConfig config, const std::size_t lower,
+    const std::size_t upper) {
+  // Depth-optimal synthesis is achieved by determining a timestep limit T such
+  // that there exists a solution with depth T, but no solution with depth T-1.
+  // This procedure uses an encoding where multiple gates are allowed per
+  // timestep (as long as they can be executed in parallel). This procedure is
+  // guaranteed to produce a depth-optimal circuit. However, the number of gates
+  // in the resulting circuit is not necessarily minimal, i.e., there may be a
+  // solution with fewer gates and the same depth. To this end, an optimization
+  // pass is provided that additionally minimizes the number of gates.
+
+  if (configuration.useMaxSAT) {
+    // The MaxSAT solver can determine the optimal T with a single call by
+    // minimizing over the layers of gates (=timesteps) in the resulting
+    // circuit.
+    runMaxSAT(config);
+  } else {
+    // The binary search approach calls the SAT solver repeatedly with varying
+    // timestep (=depth) limits T until a solution with depth T is found, but no
+    // solution with depth T-1 could be determined.
+    runBinarySearch(config.timestepLimit, lower, upper, config);
+  }
+
+  if (configuration.minimizeGatesAfterDepthOptimization) {
+    // To find a solution with fewer gates, we run the solver once more with a
+    // fixed depth limit and the goal to minimize the number of gates.
+    minimizeGatesFixedDepth(config);
+  }
+}
+
+void CliffordSynthesizer::minimizeGatesFixedDepth(EncoderConfig config) {
+  if (results.getDepth() == 0U) {
+    return;
+  }
+
+  if (results.getDepth() == results.getGates()) {
+    return;
+  }
+
+  INFO() << "Found a depth-optimal circuit with depth " << results.getDepth()
+         << " and " << results.getGates()
+         << " gate(s). Trying to minimize the number of gates.";
+
+  config.targetMetric         = TargetMetric::GATES;
+  config.timestepLimit        = results.getDepth();
+  config.useMultiGateEncoding = true;
+  config.useMaxSAT            = configuration.useMaxSAT;
+
+  if (config.useMaxSAT) {
+    runMaxSAT(config);
+  } else {
+    config.gateLimit = results.getGates();
+    runBinarySearch(*config.gateLimit, results.getDepth(), results.getGates(),
+                    config);
+  }
+  INFO() << "Found a depth " << results.getDepth() << " circuit with "
+         << results.getGates() << " gate(s).";
+}
+
+void CliffordSynthesizer::twoQubitGateOptimalSynthesis(
+    EncoderConfig config, const std::size_t lower, const std::size_t upper) {
+  // Two-qubit gate-optimal synthesis is achieved by minimizing over the number
+  // of two-qubit gates. This procedure uses the same encoding as gate-optimal
+  // synthesis, but with a different objective function. In contrast to the
+  // gate-optimal synthesis, this procedure is only guaranteed to produce a
+  // two-qubit gate-optimal circuit with respect to a given timestep limit T.
+  // There might be a solution with fewer two-qubit gates that requires more
+  // gates overall. To this end, an optimization pass is provided that explores
+  // whether increasing the timestep limit can reduce the number of two-qubit
+  // gates. Furthermore, the number of gates in the resulting circuit is not
+  // necessarily minimal, i.e., there may be a solution with fewer gates and the
+  // same number of two-qubit gates. To this end, a further optimization pass is
+  // provided that additionally minimizes the number of gates.
+
+  if (configuration.useMaxSAT) {
+    // The MaxSAT solver can determine the optimal number of two-qubit gates
+    // with a single call by minimizing over the number of two-qubit gate
+    // variables.
+    runMaxSAT(config);
+  } else {
+    // The binary search approach calls the SAT solver repeatedly with varying
+    // two-qubit gate count limits G until a solution with G two-qubit gates is
+    // found, but no solution with G-1 two-qubit gates could be determined.
+    config.twoQubitGateLimit = upper;
+    runBinarySearch(*config.twoQubitGateLimit, lower, upper, config);
+  }
+
+  // To find a solution with even fewer two-qubit gates but more gates overall,
+  // we run the solver once more with an increased gate count limit.
+  if (configuration.tryHigherGateLimitForTwoQubitGateOptimization) {
+    const auto gateLimit =
+        std::max(static_cast<std::size_t>(
+                     std::round(static_cast<double>(results.getGates()) *
+                                configuration.gateLimitFactor)),
+                 results.getGates() + 1U);
+    minimizeTwoQubitGatesFixedGateCount(gateLimit, config);
+  }
+
+  // While the solution at this point is optimal with respect to the number of
+  // two-qubit gates, it is possible that there is a solution with fewer gates
+  // overall. To find such a solution, we run the solver once more with a
+  // fixed limit on the number of two-qubit gates and the goal to minimize the
+  // number of gates overall.
+  if (configuration.minimizeGatesAfterTwoQubitGateOptimization) {
+    minimizeGatesFixedTwoQubitGateCount(config);
+  }
+}
+
+void CliffordSynthesizer::minimizeTwoQubitGatesFixedGateCount(
+    const std::size_t gateCount, CliffordSynthesizer::EncoderConfig config) {
+  if (results.getTwoQubitGates() == 0U) {
+    return;
+  }
+
+  INFO() << "Trying to find a solution with less than "
+         << results.getTwoQubitGates() << " two-qubit gates and at most "
+         << gateCount << " gates.";
+
+  config.targetMetric         = TargetMetric::TWO_QUBIT_GATES;
+  config.timestepLimit        = gateCount;
+  config.useMultiGateEncoding = false;
+  config.useMaxSAT            = true;
+  config.twoQubitGateLimit    = results.getTwoQubitGates() - 1U;
+
+  runMaxSAT(config);
+
+  INFO() << "Found a circuit with " << results.getTwoQubitGates()
+         << " two-qubit gate(s) and " << results.getGates()
+         << " gate(s) overall.";
+}
+
+void CliffordSynthesizer::minimizeGatesFixedTwoQubitGateCount(
+    CliffordSynthesizer::EncoderConfig config) {
+  if (results.getGates() == 0U) {
+    return;
+  }
+
+  if (results.getTwoQubitGates() == results.getGates()) {
+    return;
+  }
+
+  INFO() << "Found a two-qubit gate-count-optimal circuit with "
+         << results.getTwoQubitGates() << " two-qubit gate(s) and "
+         << results.getGates()
+         << " gate(s) overall. Trying to minimize the number of gates.";
+
+  config.targetMetric         = TargetMetric::GATES;
+  config.timestepLimit        = results.getGates();
+  config.useMultiGateEncoding = false;
+  config.useMaxSAT            = configuration.useMaxSAT;
+  config.twoQubitGateLimit    = results.getTwoQubitGates();
+
+  if (config.useMaxSAT) {
+    runMaxSAT(config);
+  } else {
+    runBinarySearch(config.timestepLimit, results.getTwoQubitGates(),
+                    results.getGates(), config);
+  }
+  INFO() << "Found a circuit with " << results.getTwoQubitGates()
+         << " two-qubit gate(s) and " << results.getGates()
+         << " gate(s) overall.";
+}
+
+void CliffordSynthesizer::runMaxSAT(const EncoderConfig& config) {
+  INFO() << "Running MaxSAT scheme with timestep limit "
+         << config.timestepLimit;
+  const auto r = callSolver(config);
+  if (r.sat()) {
+    INFO() << "Found a solution.";
+  } else {
+    INFO() << "No solution found.";
+  }
+  updateResults(configuration, r, results);
+}
+
+Results CliffordSynthesizer::callSolver(const EncoderConfig& config) {
+  ++solverCalls;
+  auto encoder = encoding::SATEncoder(config);
+  return encoder.run();
+}
+
+void CliffordSynthesizer::updateResults(const Configuration& config,
+                                        const Results&       newResults,
+                                        Results&             currentResults) {
+  if (!newResults.sat()) {
+    return;
+  }
+
+  switch (config.target) {
+  case TargetMetric::GATES:
+    if ((newResults.getGates() < currentResults.getGates()) ||
+        ((newResults.getGates() == currentResults.getGates()) &&
+         (newResults.getTwoQubitGates() < currentResults.getTwoQubitGates()))) {
+      currentResults = newResults;
+    }
+    break;
+  case TargetMetric::TWO_QUBIT_GATES:
+    if ((newResults.getTwoQubitGates() < currentResults.getTwoQubitGates()) ||
+        ((newResults.getTwoQubitGates() == currentResults.getTwoQubitGates()) &&
+         (newResults.getGates() < currentResults.getGates()))) {
+      currentResults = newResults;
+    }
+    break;
+  case TargetMetric::DEPTH:
+    if ((newResults.getDepth() < currentResults.getDepth()) ||
+        ((newResults.getDepth() == currentResults.getDepth()) &&
+         (newResults.getGates() < currentResults.getGates()))) {
+      currentResults = newResults;
+    }
+    break;
+  }
+}
+} // namespace cs
diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp
index d92821ff2..44b6d9271 100644
--- a/src/cliffordsynthesis/Tableau.cpp
+++ b/src/cliffordsynthesis/Tableau.cpp
@@ -151,7 +151,7 @@ void Tableau::fromString(const std::string& str) {
   if (line.empty()) {
     return;
   }
-  const auto  rStabilizer = std::regex("([\\+-])([IYZX]+)");
+  const auto  rStabilizer = std::regex("([\\+-]?)([IYZX]+)");
   std::smatch m;
   if (std::regex_search(line, rStabilizer)) {
     // string is a list of stabilizers
diff --git a/src/cliffordsynthesis/encoding/GateEncoder.cpp b/src/cliffordsynthesis/encoding/GateEncoder.cpp
new file mode 100644
index 000000000..8b82d1d10
--- /dev/null
+++ b/src/cliffordsynthesis/encoding/GateEncoder.cpp
@@ -0,0 +1,213 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#include "cliffordsynthesis/encoding/GateEncoder.hpp"
+
+#include "Encodings/Encodings.hpp"
+#include "utils/logging.hpp"
+
+namespace cs::encoding {
+
+using namespace logicbase;
+
+void GateEncoder::createSingleQubitGateVariables() {
+  DEBUG() << "Creating single-qubit gate variables.";
+  vars.gS.reserve(T);
+  for (std::size_t t = 0U; t < T; ++t) {
+    auto& timeStep = vars.gS.emplace_back();
+    timeStep.reserve(SINGLE_QUBIT_GATES.size());
+    for (const auto gate : SINGLE_QUBIT_GATES) {
+      auto& g = timeStep.emplace_back();
+      g.reserve(N);
+      for (std::size_t q = 0U; q < N; ++q) {
+        const std::string gName = "g_" + std::to_string(t) + "_" +
+                                  toString(gate) + "_" + std::to_string(q);
+        TRACE() << "Creating variable " << gName;
+        g.emplace_back(lb->makeVariable(gName));
+      }
+    }
+  }
+}
+
+void GateEncoder::createTwoQubitGateVariables() {
+  DEBUG() << "Creating two-qubit gate variables.";
+  vars.gC.reserve(T);
+  for (std::size_t t = 0U; t < T; ++t) {
+    auto& timeStep = vars.gC.emplace_back();
+    timeStep.reserve(N);
+    for (std::size_t ctrl = 0U; ctrl < N; ++ctrl) {
+      auto& control = timeStep.emplace_back();
+      control.reserve(N);
+      for (std::size_t trgt = 0U; trgt < N; ++trgt) {
+        const std::string gName = "g_" + std::to_string(t) + "_cx_" +
+                                  std::to_string(ctrl) + "_" +
+                                  std::to_string(trgt);
+        TRACE() << "Creating variable " << gName;
+        control.emplace_back(lb->makeVariable(gName));
+      }
+    }
+  }
+}
+
+void GateEncoder::Variables::collectSingleQubitGateVariables(
+    const std::size_t pos, const std::size_t qubit,
+    LogicVector& variables) const {
+  const auto& singleQubitGates = gS[pos];
+  for (const auto& gate : singleQubitGates) {
+    variables.emplace_back(gate[qubit]);
+  }
+}
+
+void GateEncoder::Variables::collectTwoQubitGateVariables(
+    const std::size_t pos, const std::size_t qubit, const bool target,
+    LogicVector& variables) const {
+  const auto& twoQubitGates = gC[pos];
+  const auto  n             = twoQubitGates.size();
+  for (std::size_t q = 0; q < n; ++q) {
+    if (q == qubit) {
+      continue;
+    }
+    if (target) {
+      variables.emplace_back(twoQubitGates[q][qubit]);
+    } else {
+      variables.emplace_back(twoQubitGates[qubit][q]);
+    }
+  }
+}
+
+void GateEncoder::assertExactlyOne(const LogicVector& variables) const {
+  const auto variableGrouping = encodings::groupVars(variables, 3U);
+  lb->assertFormula(encodings::exactlyOneCmdr(variableGrouping,
+                                              LogicTerm::noneTerm(), lb.get()));
+}
+
+void GateEncoder::extractCircuitFromModel(Results& res, Model& model) {
+  std::size_t nSingleQubitGates = 0U;
+  std::size_t nTwoQubitGates    = 0U;
+
+  qc::QuantumComputation qc(N);
+  for (std::size_t t = 0; t < T; ++t) {
+    extractSingleQubitGatesFromModel(t, model, qc, nSingleQubitGates);
+    extractTwoQubitGatesFromModel(t, model, qc, nTwoQubitGates);
+  }
+
+  res.setSingleQubitGates(nSingleQubitGates);
+  res.setTwoQubitGates(nTwoQubitGates);
+  res.setDepth(qc.getDepth());
+  res.setResultCircuit(qc);
+}
+
+void GateEncoder::extractSingleQubitGatesFromModel(
+    const std::size_t pos, Model& model, qc::QuantumComputation& qc,
+    std::size_t& nSingleQubitGates) {
+  const auto& singleQubitGates = vars.gS[pos];
+  for (std::size_t q = 0U; q < N; ++q) {
+    for (const auto gate : SINGLE_QUBIT_GATES) {
+      if (gate == qc::OpType::None) {
+        continue;
+      }
+      if (model.getBoolValue(singleQubitGates[gateToIndex(gate)][q],
+                             lb.get())) {
+        qc.emplace_back<qc::StandardOperation>(N, q, gate);
+        ++nSingleQubitGates;
+        DEBUG() << toString(gate) << "(" << q << ")";
+      }
+    }
+  }
+}
+
+void GateEncoder::extractTwoQubitGatesFromModel(const std::size_t       pos,
+                                                Model&                  model,
+                                                qc::QuantumComputation& qc,
+                                                size_t& nTwoQubitGates) {
+  const auto& twoQubitGates = vars.gC[pos];
+  for (std::size_t ctrl = 0U; ctrl < N; ++ctrl) {
+    for (std::size_t trgt = 0U; trgt < N; ++trgt) {
+      if (ctrl == trgt) {
+        continue;
+      }
+      const auto control =
+          dd::Control{static_cast<dd::Qubit>(ctrl), dd::Control::Type::pos};
+      if (model.getBoolValue(twoQubitGates[ctrl][trgt], lb.get())) {
+        qc.emplace_back<qc::StandardOperation>(N, control, trgt, qc::OpType::X);
+        ++nTwoQubitGates;
+        DEBUG() << "CX(" << ctrl << ", " << trgt << ")";
+      }
+    }
+  }
+}
+
+void GateEncoder::encodeSymmetryBreakingConstraints() {
+  DEBUG() << "Encoding symmetry breaking constraints.";
+  for (std::size_t t = 0U; t < T; ++t) {
+    assertSingleQubitGateSymmetryBreakingConstraints(t);
+    assertTwoQubitGateSymmetryBreakingConstraints(t);
+  }
+}
+
+void GateEncoder::assertSingleQubitGateCancellationConstraints(
+    const std::size_t pos, const std::size_t qubit) {
+  // nothing to assert for the last timestep
+  if (pos == T - 1U) {
+    return;
+  }
+
+  // gate variables of the current and the next timestep
+  const auto& gSNow  = vars.gS[pos];
+  const auto& gSNext = vars.gS[pos + 1U];
+
+  for (const auto gate : SINGLE_QUBIT_GATES) {
+    if (gate == qc::OpType::None) {
+      continue;
+    }
+    const auto gateIndex = gateToIndex(gate);
+    switch (gate) {
+    case qc::OpType::X:
+    case qc::OpType::Y:
+    case qc::OpType::Z:
+    case qc::OpType::H:
+      // self-inverse gates
+      lb->assertFormula(LogicTerm::implies(gSNow[gateIndex][qubit],
+                                           !gSNext[gateIndex][qubit]));
+      break;
+    case qc::OpType::S:
+    case qc::OpType::Sdag: {
+      // Sdag * S = S * Sdag = I
+      // Sdag * Sdag = S * S = Z
+      auto disallowed = !gSNext[gateToIndex(qc::OpType::S)][qubit] &&
+                        !gSNext[gateToIndex(qc::OpType::Sdag)][qubit];
+      // Z and Sdag commute. Z should always precede S and Sdag
+      disallowed = disallowed && !gSNext[gateToIndex(qc::OpType::Z)][qubit];
+      lb->assertFormula(
+          LogicTerm::implies(gSNow[gateIndex][qubit], disallowed));
+      break;
+    }
+    default:
+      break;
+    }
+  }
+}
+
+void GateEncoder::assertSingleQubitGateSymmetryBreakingConstraints(
+    const std::size_t pos) {
+  for (std::size_t q = 0U; q < N; ++q) {
+    assertSingleQubitGateOrderConstraints(pos, q);
+    assertSingleQubitGateCancellationConstraints(pos, q);
+  }
+}
+
+void GateEncoder::assertTwoQubitGateSymmetryBreakingConstraints(
+    const std::size_t pos) {
+  for (std::size_t ctrl = 0U; ctrl < N; ++ctrl) {
+    for (std::size_t trgt = 0U; trgt < N; ++trgt) {
+      if (ctrl == trgt) {
+        continue;
+      }
+      assertTwoQubitGateOrderConstraints(pos, ctrl, trgt);
+    }
+  }
+}
+
+} // namespace cs::encoding
diff --git a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp
new file mode 100644
index 000000000..8a7b8cfc5
--- /dev/null
+++ b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp
@@ -0,0 +1,160 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#include "cliffordsynthesis/encoding/MultiGateEncoder.hpp"
+
+#include "LogicTerm/LogicTerm.hpp"
+#include "utils/logging.hpp"
+
+namespace cs::encoding {
+
+using namespace logicbase;
+
+void encoding::MultiGateEncoder::assertConsistency() const {
+  DEBUG() << "Asserting gate consistency";
+  for (std::size_t t = 0U; t < T; ++t) {
+    // asserting only a single gate is applied on each qubit.
+    for (std::size_t q = 0U; q < N; ++q) {
+      LogicVector gateVariables{};
+      vars.collectSingleQubitGateVariables(t, q, gateVariables);
+      vars.collectTwoQubitGateVariables(t, q, true, gateVariables);
+      vars.collectTwoQubitGateVariables(t, q, false, gateVariables);
+
+      IF_PLOG(plog::verbose) {
+        TRACE() << "Gate variables at time " << t << " and qubit " << q;
+        for (const auto& var : gateVariables) {
+          TRACE() << var.getName();
+        }
+      }
+
+      assertExactlyOne(gateVariables);
+    }
+  }
+}
+
+void encoding::MultiGateEncoder::assertGateConstraints() {
+  DEBUG() << "Asserting gate constraints";
+  for (std::size_t t = 0U; t < T; ++t) {
+    TRACE() << "Asserting gate constraints at time " << t;
+    rChanges = tvars->r[t];
+    assertSingleQubitGateConstraints(t);
+    assertTwoQubitGateConstraints(t);
+    TRACE() << "Asserting r changes at time " << t;
+    lb->assertFormula(tvars->r[t + 1] == rChanges);
+  }
+}
+
+void encoding::MultiGateEncoder::assertSingleQubitGateConstraints(
+    const std::size_t pos) {
+  const auto& singleQubitGates = vars.gS[pos];
+  for (std::size_t q = 0U; q < N; ++q) {
+    for (const auto gate : SINGLE_QUBIT_GATES) {
+      const auto changes = createSingleQubitGateConstraint(pos, q, gate);
+      lb->assertFormula(
+          LogicTerm::implies(singleQubitGates[gateToIndex(gate)][q], changes));
+
+      DEBUG() << "Asserting " << toString(gate) << " on " << q;
+    }
+  }
+}
+
+LogicTerm encoding::MultiGateEncoder::createSingleQubitGateConstraint(
+    const std::size_t pos, const std::size_t qubit, const qc::OpType gate) {
+  auto changes = LogicTerm(true);
+
+  changes = changes && (tvars->x[pos + 1][qubit] ==
+                        tvars->singleQubitXChange(pos, qubit, gate));
+  changes = changes && (tvars->z[pos + 1][qubit] ==
+                        tvars->singleQubitZChange(pos, qubit, gate));
+  rChanges =
+      rChanges ^ LogicTerm::ite(vars.gS[pos][gateToIndex(gate)][qubit],
+                                tvars->singleQubitRChange(pos, qubit, gate),
+                                LogicTerm(0, N));
+
+  return changes;
+}
+
+void encoding::MultiGateEncoder::assertTwoQubitGateConstraints(
+    const std::size_t pos) {
+  const auto& twoQubitGates = vars.gC[pos];
+  for (std::size_t ctrl = 0U; ctrl < N; ++ctrl) {
+    for (std::size_t trgt = 0U; trgt < N; ++trgt) {
+      if (ctrl == trgt) {
+        continue;
+      }
+      const auto changes = createTwoQubitGateConstraint(pos, ctrl, trgt);
+      lb->assertFormula(LogicTerm::implies(twoQubitGates[ctrl][trgt], changes));
+
+      DEBUG() << "Asserting CNOT on " << ctrl << " and " << trgt;
+    }
+  }
+}
+
+LogicTerm encoding::MultiGateEncoder::createTwoQubitGateConstraint(
+    std::size_t pos, std::size_t ctrl, std::size_t trgt) {
+  auto changes              = LogicTerm(true);
+  const auto [xCtrl, xTrgt] = tvars->twoQubitXChange(pos, ctrl, trgt);
+  const auto [zCtrl, zTrgt] = tvars->twoQubitZChange(pos, ctrl, trgt);
+
+  changes = changes && (tvars->x[pos + 1][ctrl] == xCtrl);
+  changes = changes && (tvars->x[pos + 1][trgt] == xTrgt);
+  changes = changes && (tvars->z[pos + 1][ctrl] == zCtrl);
+  changes = changes && (tvars->z[pos + 1][trgt] == zTrgt);
+
+  rChanges = rChanges ^ LogicTerm::ite(vars.gC[pos][ctrl][trgt],
+                                       tvars->twoQubitRChange(pos, ctrl, trgt),
+                                       LogicTerm(0, N));
+
+  return changes;
+}
+
+void MultiGateEncoder::assertSingleQubitGateOrderConstraints(
+    const std::size_t pos, const std::size_t qubit) {
+  // nothing to assert at the end
+  if (pos == T - 1U) {
+    return;
+  }
+
+  // gate variables of the current and the next time step
+  const auto& gSNow  = vars.gS[pos];
+  const auto& gSNext = vars.gS[pos + 1];
+
+  // once no gate is applied to the considered qubit, no single qubit gate can
+  // be applied to it in the next time step.
+  auto noSingleQubitGate = LogicTerm(true);
+  for (const auto gate : SINGLE_QUBIT_GATES) {
+    if (gate == qc::OpType::None) {
+      continue;
+    }
+    noSingleQubitGate = noSingleQubitGate && !gSNext[gateToIndex(gate)][qubit];
+  }
+  lb->assertFormula(LogicTerm::implies(
+      gSNow[gateToIndex(qc::OpType::None)][qubit], noSingleQubitGate));
+}
+
+void MultiGateEncoder::assertTwoQubitGateOrderConstraints(
+    const std::size_t pos, const std::size_t ctrl, const std::size_t trgt) {
+  // nothing to assert at the end
+  if (pos == T - 1U) {
+    return;
+  }
+
+  // gate variables of the current and the next time step
+  const auto& current = vars.gC[pos][ctrl][trgt];
+  const auto& gSNow   = vars.gS[pos];
+  const auto& gCNext  = vars.gC[pos + 1];
+
+  // two identical CNOTs may not be applied in a row because they would cancel.
+  lb->assertFormula(LogicTerm::implies(current, !gCNext[ctrl][trgt]));
+
+  // if no gate is applied to both qubits, no CNOT on them can be applied in the
+  // next time step.
+  const auto noneIndex     = gateToIndex(qc::OpType::None);
+  const auto noGate        = gSNow[noneIndex][ctrl] && gSNow[noneIndex][trgt];
+  const auto noFurtherCnot = !gCNext[ctrl][trgt] && !gCNext[trgt][ctrl];
+  lb->assertFormula(LogicTerm::implies(noGate, noFurtherCnot));
+}
+
+} // namespace cs::encoding
diff --git a/src/cliffordsynthesis/encoding/ObjectiveEncoder.cpp b/src/cliffordsynthesis/encoding/ObjectiveEncoder.cpp
new file mode 100644
index 000000000..d42c62fbf
--- /dev/null
+++ b/src/cliffordsynthesis/encoding/ObjectiveEncoder.cpp
@@ -0,0 +1,66 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#include "cliffordsynthesis/encoding/ObjectiveEncoder.hpp"
+
+#include "LogicTerm/LogicTerm.hpp"
+#include "cliffordsynthesis/encoding/MultiGateEncoder.hpp"
+#include "utils/logging.hpp"
+
+namespace cs::encoding {
+
+using namespace logicbase;
+
+LogicTerm
+ObjectiveEncoder::collectGateCount(const bool includeSingleQubitGates) const {
+  auto cost = LogicTerm(0);
+  for (std::size_t t = 0U; t < T; ++t) {
+    if (includeSingleQubitGates) {
+      collectSingleQubitGateTerms(t, cost, std::plus{});
+    }
+    collectTwoQubitGateTerms(t, cost, std::plus{});
+  }
+  return cost;
+}
+
+void ObjectiveEncoder::optimizeGateCount(
+    const bool includeSingleQubitGates) const {
+  DEBUG() << "Optimizing " << (includeSingleQubitGates ? "" : "two-qubit ")
+          << "gate count";
+  const auto cost = collectGateCount(includeSingleQubitGates);
+  dynamic_cast<LogicBlockOptimizer*>(lb.get())->minimize(cost);
+}
+
+void ObjectiveEncoder::optimizeDepth(bool includeSingleQubitGates) const {
+  DEBUG() << "Optimizing " << (includeSingleQubitGates ? "" : "two-qubit ")
+          << "depth";
+  auto* optimizer = dynamic_cast<LogicBlockOptimizer*>(lb.get());
+  for (std::size_t t = 0U; t < T; ++t) {
+    auto anyGate = LogicTerm(false);
+    if (includeSingleQubitGates) {
+      collectSingleQubitGateTerms(t, anyGate, std::logical_or{});
+    }
+    collectTwoQubitGateTerms(t, anyGate, std::logical_or{});
+    optimizer->weightedTerm(anyGate, 1);
+  }
+  optimizer->makeMinimize();
+}
+
+void ObjectiveEncoder::optimizeMetric(TargetMetric targetMetric) const {
+  switch (targetMetric) {
+  case TargetMetric::GATES:
+    optimizeGateCount();
+    break;
+  case TargetMetric::TWO_QUBIT_GATES:
+    optimizeGateCount(false);
+    break;
+  case TargetMetric::DEPTH:
+    optimizeDepth();
+    break;
+  default:
+    FATAL() << "Unknown target metric: " << toString(targetMetric);
+  }
+}
+} // namespace cs::encoding
diff --git a/src/cliffordsynthesis/encoding/SATEncoder.cpp b/src/cliffordsynthesis/encoding/SATEncoder.cpp
new file mode 100644
index 000000000..cbef73268
--- /dev/null
+++ b/src/cliffordsynthesis/encoding/SATEncoder.cpp
@@ -0,0 +1,147 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#include "cliffordsynthesis/encoding/SATEncoder.hpp"
+
+#include "LogicUtil/util_logicblock.hpp"
+#include "cliffordsynthesis/encoding/MultiGateEncoder.hpp"
+#include "cliffordsynthesis/encoding/SingleGateEncoder.hpp"
+#include "utils/logging.hpp"
+
+#include <chrono>
+
+namespace cs::encoding {
+
+using namespace logicbase;
+
+void SATEncoder::initializeSolver() {
+  DEBUG() << "Initializing solver engine.";
+  bool success        = false;
+  LogicTerm::termType = TermType::BASE;
+  logicutil::Params params;
+  if (config.useMaxSAT) {
+    params.addParam("pb.compile_equality", true);
+    params.addParam("maxres.hill_climb", true);
+    params.addParam("maxres.pivot_on_correction_set", false);
+    lb = logicutil::getZ3LogicOptimizer(success, true, params);
+  } else {
+    params.addParam("threads", static_cast<std::uint32_t>(config.nThreads / 2));
+    lb = logicutil::getZ3LogicBlock(success, true, params);
+  }
+  if (!success) {
+    FATAL() << "Could not initialize solver engine.";
+  }
+}
+
+void SATEncoder::createFormulation() {
+  INFO() << "Creating formulation.";
+  const auto start = std::chrono::high_resolution_clock::now();
+  initializeSolver();
+
+  tableauEncoder = std::make_shared<TableauEncoder>(N, T, lb);
+  tableauEncoder->createTableauVariables();
+  tableauEncoder->assertTableau(*config.initialTableau, 0U);
+  tableauEncoder->assertTableau(*config.targetTableau, T);
+
+  if (config.useMultiGateEncoding) {
+    gateEncoder = std::make_shared<MultiGateEncoder>(
+        N, T, tableauEncoder->getVariables(), lb);
+  } else {
+    gateEncoder = std::make_shared<SingleGateEncoder>(
+        N, T, tableauEncoder->getVariables(), lb);
+  }
+  gateEncoder->createSingleQubitGateVariables();
+  gateEncoder->createTwoQubitGateVariables();
+  gateEncoder->encodeGates();
+
+  if (config.useSymmetryBreaking) {
+    gateEncoder->encodeSymmetryBreakingConstraints();
+  }
+
+  objectiveEncoder =
+      std::make_shared<ObjectiveEncoder>(N, T, gateEncoder->getVariables(), lb);
+
+  if (config.gateLimit.has_value()) {
+    objectiveEncoder->limitGateCount(*config.gateLimit, std::less_equal{});
+  }
+
+  if (config.twoQubitGateLimit.has_value()) {
+    objectiveEncoder->limitGateCount(*config.twoQubitGateLimit,
+                                     std::less_equal{}, false);
+  }
+
+  if (config.useMaxSAT) {
+    objectiveEncoder->optimizeMetric(config.targetMetric);
+  }
+
+  const auto end = std::chrono::high_resolution_clock::now();
+  const auto duration =
+      std::chrono::duration_cast<std::chrono::milliseconds>(end - start)
+          .count();
+  INFO() << "Formulation created in " << duration << " ms.";
+}
+
+void SATEncoder::produceInstance() const {
+  INFO() << "Generating the SAT instance.";
+  const auto start = std::chrono::high_resolution_clock::now();
+  lb->produceInstance();
+  const auto end = std::chrono::high_resolution_clock::now();
+  const auto runtime =
+      std::chrono::duration_cast<std::chrono::milliseconds>(end - start)
+          .count();
+  INFO() << "Instance generated in " << runtime << " ms.";
+
+  DEBUG() << "Instance statistics:";
+  DEBUG() << "\tClauses: " << TermImpl::getNextId(lb.get());
+  DEBUG() << "\tNone terms: " << TermImpl::getNextId();
+}
+
+Result SATEncoder::solve() const {
+  INFO() << "Solving the SAT instance.";
+  const auto start  = std::chrono::high_resolution_clock::now();
+  const auto result = lb->solve();
+  const auto end    = std::chrono::high_resolution_clock::now();
+  const auto runtime =
+      std::chrono::duration_cast<std::chrono::milliseconds>(end - start)
+          .count();
+  INFO() << "Instance solved in " << runtime << " ms.";
+  return result;
+}
+
+void SATEncoder::extractResultsFromModel(Results& res) const {
+  auto* const model = lb->getModel();
+  tableauEncoder->extractTableauFromModel(res, T, *model);
+  gateEncoder->extractCircuitFromModel(res, *model);
+}
+
+void SATEncoder::cleanup() const {
+  if (lb) {
+    lb->reset();
+  }
+}
+Results SATEncoder::run() {
+  const auto start = std::chrono::high_resolution_clock::now();
+
+  createFormulation();
+  produceInstance();
+  const auto solverResult = solve();
+
+  const auto end     = std::chrono::high_resolution_clock::now();
+  const auto runtime = std::chrono::duration<double>(end - start);
+
+  Results res{};
+  res.setRuntime(runtime.count());
+  res.setSolverResult(solverResult);
+
+  if (solverResult == Result::SAT) {
+    extractResultsFromModel(res);
+  }
+
+  cleanup();
+
+  return res;
+}
+
+} // namespace cs::encoding
diff --git a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp
new file mode 100644
index 000000000..787adbe51
--- /dev/null
+++ b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp
@@ -0,0 +1,225 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#include "cliffordsynthesis/encoding/SingleGateEncoder.hpp"
+
+#include "utils/logging.hpp"
+
+namespace cs::encoding {
+
+using namespace logicbase;
+
+void SingleGateEncoder::assertConsistency() const {
+  DEBUG() << "Asserting gate consistency";
+  for (std::size_t t = 0U; t < T; ++t) {
+    LogicVector gateVariables{};
+
+    for (std::size_t q = 0U; q < N; ++q) {
+      vars.collectSingleQubitGateVariables(t, q, gateVariables);
+      vars.collectTwoQubitGateVariables(t, q, true, gateVariables);
+    }
+    IF_PLOG(plog::verbose) {
+      TRACE() << "Gate variables at time " << t;
+      for (const auto& var : gateVariables) {
+        TRACE() << var.getName();
+      }
+    }
+    assertExactlyOne(gateVariables);
+  }
+}
+
+void SingleGateEncoder::assertGateConstraints() {
+  DEBUG() << "Asserting gate constraints";
+  for (std::size_t t = 0U; t < T; ++t) {
+    TRACE() << "Asserting gate constraints at time " << t;
+    assertSingleQubitGateConstraints(t);
+    assertTwoQubitGateConstraints(t);
+  }
+}
+
+void SingleGateEncoder::assertSingleQubitGateConstraints(std::size_t pos) {
+  const auto& singleQubitGates = vars.gS[pos];
+  for (std::size_t q = 0U; q < N; ++q) {
+    for (const auto gate : SINGLE_QUBIT_GATES) {
+      const auto changes = createSingleQubitGateConstraint(pos, q, gate);
+
+      DEBUG() << "Asserting " << toString(gate) << " on " << q;
+
+      lb->assertFormula(
+          LogicTerm::implies(singleQubitGates[gateToIndex(gate)][q], changes));
+    }
+  }
+}
+
+LogicTerm SingleGateEncoder::createSingleQubitGateConstraint(
+    const std::size_t pos, const std::size_t qubit, const qc::OpType gate) {
+  auto changes = LogicTerm(true);
+
+  changes = changes && (tvars->x[pos + 1][qubit] ==
+                        tvars->singleQubitXChange(pos, qubit, gate));
+  changes = changes && (tvars->z[pos + 1][qubit] ==
+                        tvars->singleQubitZChange(pos, qubit, gate));
+  changes = changes &&
+            (tvars->r[pos + 1] ==
+             (tvars->r[pos] ^ tvars->singleQubitRChange(pos, qubit, gate)));
+
+  return changes && createNoChange(pos, qubit, std::nullopt);
+}
+
+void SingleGateEncoder::assertTwoQubitGateConstraints(const std::size_t pos) {
+  const auto& twoQubitGates = vars.gC[pos];
+  for (std::size_t ctrl = 0U; ctrl < N; ++ctrl) {
+    for (std::size_t trgt = 0U; trgt < N; ++trgt) {
+      if (ctrl == trgt) {
+        continue;
+      }
+      const auto changes = createTwoQubitGateConstraint(pos, ctrl, trgt);
+
+      DEBUG() << "Asserting CNOT on " << ctrl << " and " << trgt;
+
+      lb->assertFormula(LogicTerm::implies(twoQubitGates[ctrl][trgt], changes));
+    }
+  }
+}
+
+LogicTerm SingleGateEncoder::createTwoQubitGateConstraint(
+    const std::size_t pos, const std::size_t ctrl, const std::size_t trgt) {
+  auto changes              = LogicTerm(true);
+  const auto [xCtrl, xTrgt] = tvars->twoQubitXChange(pos, ctrl, trgt);
+  const auto [zCtrl, zTrgt] = tvars->twoQubitZChange(pos, ctrl, trgt);
+
+  changes = changes && (tvars->x[pos + 1][ctrl] == xCtrl);
+  changes = changes && (tvars->x[pos + 1][trgt] == xTrgt);
+  changes = changes && (tvars->z[pos + 1][ctrl] == zCtrl);
+  changes = changes && (tvars->z[pos + 1][trgt] == zTrgt);
+  changes =
+      changes && (tvars->r[pos + 1] ==
+                  (tvars->r[pos] ^ tvars->twoQubitRChange(pos, ctrl, trgt)));
+
+  return changes && createNoChange(pos, ctrl, trgt);
+}
+
+LogicTerm SingleGateEncoder::createNoChange(
+    const std::size_t pos, const std::size_t except,
+    const std::optional<std::size_t> except2) const {
+  auto changes = LogicTerm(true);
+  for (std::size_t q = 0U; q < N; ++q) {
+    if (q == except) {
+      continue;
+    }
+    if (except2.has_value() && q == except2.value()) {
+      continue;
+    }
+
+    changes = changes && (tvars->x[pos + 1][q] == tvars->x[pos][q]);
+    changes = changes && (tvars->z[pos + 1][q] == tvars->z[pos][q]);
+  }
+  return changes;
+}
+
+void SingleGateEncoder::assertSingleQubitGateOrderConstraints(
+    const std::size_t pos, const std::size_t qubit) {
+  // nothing to assert at the end
+  if (pos == T - 1U) {
+    return;
+  }
+
+  // gate variables of the current and the next time step
+  const auto& gSNow  = vars.gS[pos];
+  const auto& gSNext = vars.gS[pos + 1];
+
+  // collect variables of single-qubit gates that could be applied to `qubit`
+  auto singleQubitGate = LogicTerm(false);
+  for (const auto& gate : SINGLE_QUBIT_GATES) {
+    if (gate == qc::OpType::None) {
+      continue;
+    }
+    // any single-qubit gate on qubit q
+    singleQubitGate = singleQubitGate || gSNow[gateToIndex(gate)][qubit];
+  }
+
+  // collect gate variables of the next timestep that should not be applied.
+  auto disallowed = LogicTerm(true);
+
+  // no single-qubit gate on a lower qubit
+  for (std::size_t lower = 0U; lower < qubit; ++lower) {
+    for (const auto& gate : SINGLE_QUBIT_GATES) {
+      if (gate == qc::OpType::None) {
+        continue;
+      }
+      disallowed = disallowed && !gSNext[gateToIndex(gate)][lower];
+    }
+  }
+
+  lb->assertFormula(LogicTerm::implies(singleQubitGate, disallowed));
+
+  // once no gate is applied, no other gate can be applied, i.e., in the next
+  // timestep any of the `None` gate variables must be selected.
+  const auto noneIndex = gateToIndex(qc::OpType::None);
+  auto       noGate    = LogicTerm(false);
+  for (std::size_t q = 0U; q < N; ++q) {
+    noGate = noGate || gSNext[noneIndex][q];
+  }
+  lb->assertFormula(LogicTerm::implies(gSNow[noneIndex][qubit], noGate));
+}
+
+void SingleGateEncoder::assertTwoQubitGateOrderConstraints(
+    const std::size_t pos, const std::size_t ctrl, const std::size_t trgt) {
+  // nothing to assert at the end
+  if (pos == T - 1U) {
+    return;
+  }
+
+  // gate variables of the current and the next time step
+  const auto& current = vars.gC[pos][ctrl][trgt];
+  const auto& gCNext  = vars.gC[pos + 1];
+  const auto& gSNext  = vars.gS[pos + 1];
+
+  // two identical CNOTs may not be applied in a row because they would cancel.
+  auto disallowed = !gCNext[ctrl][trgt];
+
+  // any single-qubit gate independent of the CNOT should be applied prior.
+  for (std::size_t q = 0U; q < N; ++q) {
+    if (q == ctrl || q == trgt) {
+      continue;
+    }
+    for (const auto& gate : SINGLE_QUBIT_GATES) {
+      if (gate == qc::OpType::None) {
+        continue;
+      }
+      disallowed = disallowed && !gSNext[gateToIndex(gate)][q];
+    }
+  }
+
+  // no X gate may be placed on the target qubit since it would commute.
+  disallowed = disallowed && !gSNext[gateToIndex(qc::OpType::X)][trgt];
+
+  // no diagonal gate may be placed on the control qubit since it would commute.
+  disallowed = disallowed && !gSNext[gateToIndex(qc::OpType::Z)][ctrl] &&
+               !gSNext[gateToIndex(qc::OpType::S)][ctrl] &&
+               !gSNext[gateToIndex(qc::OpType::Sdag)][ctrl];
+
+  // no CNOT with the same control and a lower target qubit may be placed.
+  for (std::size_t t = 0U; t < trgt; ++t) {
+    if (t == ctrl) {
+      continue;
+    }
+    disallowed = disallowed && !gCNext[ctrl][t];
+  }
+
+  // no CNOT with a lower control different from trgt may be placed.
+  for (std::size_t c = 0U; c < ctrl; ++c) {
+    for (std::size_t t = 0U; t < N; ++t) {
+      if (c == t || c == trgt) {
+        continue;
+      }
+      disallowed = disallowed && !gCNext[c][t];
+    }
+  }
+
+  lb->assertFormula(LogicTerm::implies(current, disallowed));
+}
+
+} // namespace cs::encoding
diff --git a/src/cliffordsynthesis/encoding/TableauEncoder.cpp b/src/cliffordsynthesis/encoding/TableauEncoder.cpp
new file mode 100644
index 000000000..d6e0e74c8
--- /dev/null
+++ b/src/cliffordsynthesis/encoding/TableauEncoder.cpp
@@ -0,0 +1,167 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#include "cliffordsynthesis/encoding/TableauEncoder.hpp"
+
+#include "utils/logging.hpp"
+
+namespace cs::encoding {
+
+using namespace logicbase;
+
+void TableauEncoder::createTableauVariables() {
+  const auto n = static_cast<std::int16_t>(N);
+
+  DEBUG() << "Creating tableau variables.";
+  vars.x.reserve(T);
+  vars.z.reserve(T);
+  vars.r.reserve(T);
+  for (std::size_t t = 0U; t <= T; ++t) {
+    auto& x = vars.x.emplace_back();
+    auto& z = vars.z.emplace_back();
+    x.reserve(N);
+    z.reserve(N);
+    for (std::size_t i = 0U; i < N; ++i) {
+      const std::string xName =
+          "x_" + std::to_string(t) + "_" + std::to_string(i);
+      TRACE() << "Creating variable " << xName;
+      x.emplace_back(lb->makeVariable(xName, CType::BITVECTOR, n));
+      const std::string zName =
+          "z_" + std::to_string(t) + "_" + std::to_string(i);
+      TRACE() << "Creating variable " << zName;
+      z.emplace_back(lb->makeVariable(zName, CType::BITVECTOR, n));
+    }
+    const std::string rName = "r_" + std::to_string(t);
+    TRACE() << "Creating variable " << rName;
+    vars.r.emplace_back(lb->makeVariable(rName, CType::BITVECTOR, n));
+  }
+}
+
+void TableauEncoder::assertTableau(const Tableau&    tableau,
+                                   const std::size_t t) {
+  const auto n = static_cast<std::int16_t>(N);
+
+  DEBUG() << "Asserting tableau at time step " << t;
+  TRACE() << "Tableau:\n" << tableau;
+  for (auto a = 0U; a < N; ++a) {
+    const auto targetX = tableau.getBVFrom(a);
+    lb->assertFormula(vars.x[t][a] == LogicTerm(targetX, n));
+
+    const auto targetZ = tableau.getBVFrom(a + N);
+    lb->assertFormula(vars.z[t][a] == LogicTerm(targetZ, n));
+  }
+
+  const auto targetR = tableau.getBVFrom(2U * N);
+  lb->assertFormula(vars.r[t] == LogicTerm(targetR, n));
+}
+
+void TableauEncoder::extractTableauFromModel(Results&          results,
+                                             const std::size_t t,
+                                             Model&            model) const {
+  Tableau tableau(N);
+  for (std::size_t i = 0; i < N; ++i) {
+    const auto bvx = model.getBitvectorValue(vars.x[t][i], lb.get());
+    tableau.populateTableauFrom(bvx, N, i);
+    const auto bvz = model.getBitvectorValue(vars.z[t][i], lb.get());
+    tableau.populateTableauFrom(bvz, N, i + N);
+  }
+  const auto bvr = model.getBitvectorValue(vars.r[t], lb.get());
+  tableau.populateTableauFrom(bvr, N, 2 * N);
+
+  results.setResultTableau(tableau);
+}
+
+LogicTerm
+TableauEncoder::Variables::singleQubitXChange(const std::size_t pos,
+                                              const std::size_t qubit,
+                                              const qc::OpType  gate) const {
+  switch (gate) {
+  case qc::OpType::None:
+  case qc::OpType::X:
+  case qc::OpType::Y:
+  case qc::OpType::Z:
+  case qc::OpType::S:
+  case qc::OpType::Sdag:
+    return x[pos][qubit];
+  case qc::OpType::H:
+    return z[pos][qubit];
+  default:
+    FATAL() << "Unsupported single-qubit gate: " << toString(gate);
+    return LogicTerm::noneTerm();
+  }
+}
+
+LogicTerm
+TableauEncoder::Variables::singleQubitZChange(const std::size_t pos,
+                                              const std::size_t qubit,
+                                              const qc::OpType  gate) const {
+  switch (gate) {
+  case qc::OpType::None:
+  case qc::OpType::X:
+  case qc::OpType::Y:
+  case qc::OpType::Z:
+    return z[pos][qubit];
+  case qc::OpType::H:
+    return x[pos][qubit];
+  case qc::OpType::S:
+  case qc::OpType::Sdag:
+    return (z[pos][qubit] ^ x[pos][qubit]);
+  default:
+    FATAL() << "Unsupported single-qubit gate: " << toString(gate);
+    return LogicTerm::noneTerm();
+  }
+}
+
+LogicTerm
+TableauEncoder::Variables::singleQubitRChange(const std::size_t pos,
+                                              const std::size_t qubit,
+                                              const qc::OpType  gate) const {
+  switch (gate) {
+  case qc::OpType::None: {
+    const auto bvs = r[pos].getBitVectorSize();
+    return {0, bvs};
+  }
+  case qc::OpType::H:
+  case qc::OpType::S:
+    return x[pos][qubit] & z[pos][qubit];
+  case qc::OpType::Sdag:
+    return x[pos][qubit] & (x[pos][qubit] ^ z[pos][qubit]);
+  case qc::OpType::X:
+    return z[pos][qubit];
+  case qc::OpType::Y:
+    return x[pos][qubit] ^ z[pos][qubit];
+  case qc::OpType::Z:
+    return x[pos][qubit];
+  default:
+    FATAL() << "Unsupported single-qubit gate: " << toString(gate);
+    return LogicTerm::noneTerm();
+  }
+}
+
+std::pair<LogicTerm, LogicTerm>
+TableauEncoder::Variables::twoQubitXChange(const std::size_t pos,
+                                           const std::size_t ctrl,
+                                           const std::size_t trgt) const {
+  return {x[pos][ctrl], x[pos][ctrl] ^ x[pos][trgt]};
+}
+
+std::pair<LogicTerm, LogicTerm>
+TableauEncoder::Variables::twoQubitZChange(const std::size_t pos,
+                                           const std::size_t ctrl,
+                                           const std::size_t trgt) const {
+  return {z[pos][ctrl] ^ z[pos][trgt], z[pos][trgt]};
+}
+
+LogicTerm
+TableauEncoder::Variables::twoQubitRChange(const std::size_t pos,
+                                           const std::size_t ctrl,
+                                           const std::size_t trgt) const {
+  const auto bvs = r[pos].getBitVectorSize();
+  const auto one = LogicTerm((1ULL << bvs) - 1, bvs);
+
+  return (x[pos][ctrl] & z[pos][trgt]) & ((z[pos][ctrl] ^ x[pos][trgt]) ^ one);
+}
+
+} // namespace cs::encoding


Test patch:
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index ff7dc8143..32c2d4459 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -76,6 +76,12 @@ if(TARGET ${PROJECT_NAME}_exact_lib)
 endif()
 
 if(TARGET ${PROJECT_NAME}_cliffordsynthesis_lib)
-  package_add_test(${PROJECT_NAME}_cliffordsynthesis_test cliffordsynthesis
-                   ${CMAKE_CURRENT_SOURCE_DIR}/test_tableau.cpp)
+  configure_file(${CMAKE_SOURCE_DIR}/test/cliffordsynthesis/tableaus.json
+                 ${CMAKE_CURRENT_BINARY_DIR}/cliffordsynthesis/tableaus.json COPYONLY)
+  configure_file(${CMAKE_SOURCE_DIR}/test/cliffordsynthesis/circuits.json
+                 ${CMAKE_CURRENT_BINARY_DIR}/cliffordsynthesis/circuits.json COPYONLY)
+  package_add_test(
+    ${PROJECT_NAME}_cliffordsynthesis_test cliffordsynthesis
+    ${CMAKE_CURRENT_SOURCE_DIR}/test_tableau.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/cliffordsynthesis/test_synthesis.cpp)
 endif()
diff --git a/test/cliffordsynthesis/circuits.json b/test/cliffordsynthesis/circuits.json
new file mode 100644
index 000000000..00fb48e24
--- /dev/null
+++ b/test/cliffordsynthesis/circuits.json
@@ -0,0 +1,47 @@
+[
+  {
+    "description": "empty_circuit",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[1];\n",
+    "expected_minimal_gates": 0,
+    "expected_minimal_depth": 0,
+    "expected_minimal_gates_at_minimal_depth": 0,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 0
+  },
+  {
+    "description": "switched_cnot",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[2];h q; cx q[1], q[0];h q;\n",
+    "expected_minimal_gates": 1,
+    "expected_minimal_depth": 1,
+    "expected_minimal_gates_at_minimal_depth": 1,
+    "expected_minimal_two_qubit_gates": 1,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 1
+  },
+  {
+    "description": "h_h_h_h",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[1];h q;h q;h q;h q;\n",
+    "expected_minimal_gates": 0,
+    "expected_minimal_depth": 0,
+    "expected_minimal_gates_at_minimal_depth": 0,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 0
+  },
+  {
+    "description": "swap_cx",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[2];swap q[0], q[1]; cx q[0], q[1];\n",
+    "expected_minimal_gates": 2,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 2,
+    "expected_minimal_two_qubit_gates": 2,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 2
+  },
+  {
+    "description": "commutation_simplification",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[2];x q; z q[0];cz q[0], q[1]; z q[0];\n",
+    "expected_minimal_gates": 2,
+    "expected_minimal_depth": 1,
+    "expected_minimal_gates_at_minimal_depth": 2,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 2
+  }
+]
diff --git a/test/cliffordsynthesis/tableaus.json b/test/cliffordsynthesis/tableaus.json
new file mode 100644
index 000000000..edecb882e
--- /dev/null
+++ b/test/cliffordsynthesis/tableaus.json
@@ -0,0 +1,266 @@
+[
+  {
+    "description": "Z",
+    "initial_tableau": "0;1;0;",
+    "target_tableau": "0;1;0;",
+    "expected_minimal_gates": 0,
+    "expected_minimal_depth": 0,
+    "expected_minimal_gates_at_minimal_depth": 0,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 0
+  },
+  {
+    "description": "mZ",
+    "initial_tableau": "0;1;0;",
+    "target_tableau": "0;1;1;",
+    "expected_minimal_gates": 1,
+    "expected_minimal_depth": 1,
+    "expected_minimal_gates_at_minimal_depth": 1,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 1
+  },
+  {
+    "description": "X",
+    "initial_tableau": "0;1;0;",
+    "target_tableau": "1;0;0;",
+    "expected_minimal_gates": 1,
+    "expected_minimal_depth": 1,
+    "expected_minimal_gates_at_minimal_depth": 1,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 1
+  },
+  {
+    "description": "mX",
+    "initial_tableau": "0;1;0;",
+    "target_tableau": "1;0;1;",
+    "expected_minimal_gates": 2,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 2,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 2
+  },
+  {
+    "description": "Y",
+    "initial_tableau": "0;1;0;",
+    "target_tableau": "1;1;0;",
+    "expected_minimal_gates": 2,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 2,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 2
+  },
+  {
+    "description": "mY",
+    "initial_tableau": "0;1;0;",
+    "target_tableau": "1;1;1;",
+    "expected_minimal_gates": 2,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 2,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 2
+  },
+  {
+    "description": "Y_to_Y",
+    "initial_tableau": "1;1;0;",
+    "target_tableau": "1;1;0;",
+    "expected_minimal_gates": 0,
+    "expected_minimal_depth": 0,
+    "expected_minimal_gates_at_minimal_depth": 0,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 0
+  },
+
+  {
+    "description": "ZI_IZ",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "expected_minimal_gates": 0,
+    "expected_minimal_depth": 0,
+    "expected_minimal_gates_at_minimal_depth": 0,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 0
+  },
+  {
+    "description": "ZI_mIZ",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "0;0;1;0;0\n0;0;0;1;1",
+    "expected_minimal_gates": 1,
+    "expected_minimal_depth": 1,
+    "expected_minimal_gates_at_minimal_depth": 1,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 1
+  },
+  {
+    "description": "mZI_IZ",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "0;0;1;0;1\n0;0;0;1;0",
+    "expected_minimal_gates": 1,
+    "expected_minimal_depth": 1,
+    "expected_minimal_gates_at_minimal_depth": 1,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 1
+  },
+  {
+    "description": "mZI_mIZ",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "0;0;1;0;1\n0;0;0;1;1",
+    "expected_minimal_gates": 2,
+    "expected_minimal_depth": 1,
+    "expected_minimal_gates_at_minimal_depth": 2,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 2
+  },
+
+  {
+    "description": "XI_IX",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "1;0;0;0;0\n0;1;0;0;0",
+    "expected_minimal_gates": 2,
+    "expected_minimal_depth": 1,
+    "expected_minimal_gates_at_minimal_depth": 2,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 2
+  },
+  {
+    "description": "XI_mIX",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "1;0;0;0;0\n0;1;0;0;1",
+    "expected_minimal_gates": 3,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 3,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 3
+  },
+  {
+    "description": "mXI_IX",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "1;0;0;0;1\n0;1;0;0;0",
+    "expected_minimal_gates": 3,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 3,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 3
+  },
+  {
+    "description": "mXI_mIX",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "1;0;0;0;1\n0;1;0;0;1",
+    "expected_minimal_gates": 4,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 4,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 4
+  },
+
+  {
+    "description": "YI_IY",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "1;0;1;0;0\n0;1;0;1;0",
+    "expected_minimal_gates": 4,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 4,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 4
+  },
+  {
+    "description": "YI_mIY",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "1;0;1;0;0\n0;1;0;1;1",
+    "expected_minimal_gates": 4,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 4,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 4
+  },
+  {
+    "description": "mYI_IY",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "1;0;1;0;1\n0;1;0;1;0",
+    "expected_minimal_gates": 4,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 4,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 4
+  },
+  {
+    "description": "mYI_mIY",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "1;0;1;0;1\n0;1;0;1;1",
+    "expected_minimal_gates": 4,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 4,
+    "expected_minimal_two_qubit_gates": 0,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 4
+  },
+
+  {
+    "description": "XX_ZZ",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "1;1;0;0;0\n0;0;1;1;0",
+    "expected_minimal_gates": 2,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 2,
+    "expected_minimal_two_qubit_gates": 1,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 2
+  },
+  {
+    "description": "XX_mZZ",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "1;1;0;0;0\n0;0;1;1;1",
+    "expected_minimal_gates": 3,
+    "expected_minimal_depth": 2,
+    "expected_minimal_gates_at_minimal_depth": 3,
+    "expected_minimal_two_qubit_gates": 1,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 3
+  },
+  {
+    "description": "mXX_ZZ",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "1;1;0;0;1\n0;0;1;1;0",
+    "expected_minimal_gates": 3,
+    "expected_minimal_depth": 3,
+    "expected_minimal_gates_at_minimal_depth": 3,
+    "expected_minimal_two_qubit_gates": 1,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 3
+  },
+  {
+    "description": "mXX_mZZ",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "1;1;0;0;1\n0;0;1;1;1",
+    "expected_minimal_gates": 3,
+    "expected_minimal_depth": 3,
+    "expected_minimal_gates_at_minimal_depth": 3,
+    "expected_minimal_two_qubit_gates": 1,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 3
+  },
+  {
+    "description": "IZ_ZI",
+    "initial_tableau": "0;0;1;0;0\n0;0;0;1;0",
+    "target_tableau": "0;0;0;1;0\n0;0;1;0;0",
+    "expected_minimal_gates": 3,
+    "expected_minimal_depth": 3,
+    "expected_minimal_gates_at_minimal_depth": 3,
+    "expected_minimal_two_qubit_gates": 2,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 4
+  },
+  {
+    "description": "GHZ_3",
+    "initial_tableau": "0;0;0;1;0;0;0\n0;0;0;0;1;0;0\n0;0;0;0;0;1;0",
+    "target_tableau": "1;1;1;0;0;0;0\n0;0;0;1;1;0;0\n0;0;0;0;1;1;0",
+    "expected_minimal_gates": 3,
+    "expected_minimal_depth": 3,
+    "expected_minimal_gates_at_minimal_depth": 3,
+    "expected_minimal_two_qubit_gates": 2,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 3
+  },
+  {
+    "description": "GHZ_4",
+    "initial_tableau": "0;0;0;0;1;0;0;0;0\n0;0;0;0;0;1;0;0;0\n0;0;0;0;0;0;1;0;0\n0;0;0;0;0;0;0;1;0",
+    "target_tableau": "1;1;1;1;0;0;0;0;0\n0;0;0;0;1;1;0;0;0\n0;0;0;0;0;1;1;0;0\n0;0;0;0;0;0;1;1;0",
+    "expected_minimal_gates": 4,
+    "expected_minimal_depth": 3,
+    "expected_minimal_gates_at_minimal_depth": 5,
+    "expected_minimal_two_qubit_gates": 3,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 4
+  }
+]
diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp
new file mode 100644
index 000000000..72ae46a90
--- /dev/null
+++ b/test/cliffordsynthesis/test_synthesis.cpp
@@ -0,0 +1,238 @@
+//
+// This file is part of the MQT QMAP library released under the MIT license.
+// See README.md or go to https://github.com/cda-tum/qmap for more information.
+//
+
+#include "cliffordsynthesis/CliffordSynthesizer.hpp"
+
+#include "gtest/gtest.h"
+
+namespace cs {
+
+struct TestConfiguration {
+  // given input (either as tableau or as circuit)
+  std::string description;
+  std::string initialTableau;
+  std::string targetTableau;
+  std::string initialCircuit;
+
+  // expected output
+  std::size_t expectedMinimalGates{};
+  std::size_t expectedMinimalDepth{};
+  std::size_t expectedMinimalGatesAtMinimalDepth{};
+  std::size_t expectedMinimalTwoQubitGates{};
+  std::size_t expectedMinimalGatesAtMinimalTwoQubitGates{};
+};
+
+inline void from_json(const nlohmann::json& j, TestConfiguration& test) {
+  test.description = j.at("description").get<std::string>();
+  if (j.contains("initial_tableau")) {
+    test.initialTableau = j.at("initial_tableau").get<std::string>();
+  }
+  if (j.contains("target_tableau")) {
+    test.targetTableau = j.at("target_tableau").get<std::string>();
+  }
+  if (j.contains("initial_circuit")) {
+    test.initialCircuit = j.at("initial_circuit").get<std::string>();
+  }
+
+  test.expectedMinimalGates = j.at("expected_minimal_gates").get<std::size_t>();
+  test.expectedMinimalDepth = j.at("expected_minimal_depth").get<std::size_t>();
+  test.expectedMinimalGatesAtMinimalDepth =
+      j.at("expected_minimal_gates_at_minimal_depth").get<std::size_t>();
+  test.expectedMinimalTwoQubitGates =
+      j.at("expected_minimal_two_qubit_gates").get<std::size_t>();
+  test.expectedMinimalGatesAtMinimalTwoQubitGates =
+      j.at("expected_minimal_gates_at_minimal_two_qubit_gates")
+          .get<std::size_t>();
+}
+
+static std::vector<TestConfiguration> getTests(const std::string& path) {
+  std::ifstream  input(path);
+  nlohmann::json j;
+  input >> j;
+  return j;
+}
+
+class SynthesisTest : public ::testing::TestWithParam<TestConfiguration> {
+protected:
+  void SetUp() override {
+    if (plog::get() == nullptr) {
+      util::init();
+    }
+
+    test = GetParam();
+
+    if (!test.initialCircuit.empty()) {
+      std::stringstream      ss(test.initialCircuit);
+      qc::QuantumComputation qc{};
+      qc.import(ss, qc::OpenQASM);
+      std::cout << "Initial circuit:\n" << qc;
+      targetTableau = Tableau(qc);
+      if (test.initialTableau.empty()) {
+        initialTableau = Tableau(qc.getNqubits());
+        synthesizer    = CliffordSynthesizer(qc);
+      } else {
+        initialTableau = Tableau(test.initialTableau);
+        std::cout << "Initial tableau:\n" << initialTableau;
+        synthesizer = CliffordSynthesizer(initialTableau, qc);
+      }
+    } else {
+      targetTableau = Tableau(test.targetTableau);
+      if (test.initialTableau.empty()) {
+        initialTableau = Tableau(targetTableau.getQubitCount());
+        synthesizer    = CliffordSynthesizer(targetTableau);
+      } else {
+        initialTableau = Tableau(test.initialTableau);
+        std::cout << "Initial tableau:\n" << initialTableau;
+        synthesizer = CliffordSynthesizer(initialTableau, targetTableau);
+      }
+    }
+    std::cout << "Target tableau:\n" << targetTableau;
+
+    config = Configuration();
+  }
+
+  void TearDown() override {
+    std::cout << "Results:\n" << results << "\n";
+
+    resultTableau = synthesizer.getResultTableau();
+    std::cout << "Resulting tableau:\n" << resultTableau;
+    EXPECT_EQ(resultTableau, targetTableau);
+
+    const auto& resultCircuit = synthesizer.getResultCircuit();
+    std::cout << "Resulting Circuit:\n" << resultCircuit;
+    consistencyCheck(resultCircuit);
+  }
+
+  void consistencyCheck(const qc::QuantumComputation& qc) const {
+    auto circuitTableau = initialTableau;
+    for (const auto& gate : qc) {
+      circuitTableau.applyGate(gate.get());
+    }
+    EXPECT_EQ(resultTableau, circuitTableau);
+  }
+
+  Tableau             initialTableau;
+  Tableau             targetTableau;
+  Configuration       config;
+  CliffordSynthesizer synthesizer;
+  Results             results;
+  Tableau             resultTableau;
+  TestConfiguration   test;
+};
+
+INSTANTIATE_TEST_SUITE_P(
+    Tableaus, SynthesisTest,
+    testing::ValuesIn(getTests("cliffordsynthesis/tableaus.json")),
+    [](const testing::TestParamInfo<SynthesisTest::ParamType>& info) {
+      return info.param.description;
+    });
+
+INSTANTIATE_TEST_SUITE_P(
+    Circuits, SynthesisTest,
+    testing::ValuesIn(getTests("cliffordsynthesis/circuits.json")),
+    [](const testing::TestParamInfo<SynthesisTest::ParamType>& info) {
+      return info.param.description;
+    });
+
+TEST_P(SynthesisTest, Gates) {
+  config.target = TargetMetric::GATES;
+  synthesizer.synthesize(config);
+  results = synthesizer.getResults();
+
+  EXPECT_EQ(results.getGates(), test.expectedMinimalGates);
+}
+
+TEST_P(SynthesisTest, GatesMaxSAT) {
+  config.target    = TargetMetric::GATES;
+  config.useMaxSAT = true;
+  synthesizer.synthesize(config);
+  results = synthesizer.getResults();
+
+  EXPECT_EQ(results.getGates(), test.expectedMinimalGates);
+}
+
+TEST_P(SynthesisTest, Depth) {
+  config.target = TargetMetric::DEPTH;
+  synthesizer.synthesize(config);
+  results = synthesizer.getResults();
+
+  EXPECT_EQ(results.getDepth(), test.expectedMinimalDepth);
+}
+
+TEST_P(SynthesisTest, DepthMaxSAT) {
+  config.target    = TargetMetric::DEPTH;
+  config.useMaxSAT = true;
+  synthesizer.synthesize(config);
+  results = synthesizer.getResults();
+
+  EXPECT_EQ(results.getDepth(), test.expectedMinimalDepth);
+}
+
+TEST_P(SynthesisTest, DepthMinimalGates) {
+  config.target                              = TargetMetric::DEPTH;
+  config.minimizeGatesAfterDepthOptimization = true;
+  synthesizer.synthesize(config);
+  results = synthesizer.getResults();
+
+  EXPECT_EQ(results.getDepth(), test.expectedMinimalDepth);
+  EXPECT_EQ(results.getGates(), test.expectedMinimalGatesAtMinimalDepth);
+}
+
+TEST_P(SynthesisTest, DepthMinimalGatesMaxSAT) {
+  config.target                              = TargetMetric::DEPTH;
+  config.useMaxSAT                           = true;
+  config.minimizeGatesAfterDepthOptimization = true;
+  synthesizer.synthesize(config);
+  results = synthesizer.getResults();
+
+  EXPECT_EQ(results.getDepth(), test.expectedMinimalDepth);
+  EXPECT_EQ(results.getGates(), test.expectedMinimalGatesAtMinimalDepth);
+}
+
+TEST_P(SynthesisTest, TwoQubitGates) {
+  config.target = TargetMetric::TWO_QUBIT_GATES;
+  config.tryHigherGateLimitForTwoQubitGateOptimization = true;
+  synthesizer.synthesize(config);
+  results = synthesizer.getResults();
+
+  EXPECT_EQ(results.getTwoQubitGates(), test.expectedMinimalTwoQubitGates);
+}
+
+TEST_P(SynthesisTest, TwoQubitGatesMaxSAT) {
+  config.target = TargetMetric::TWO_QUBIT_GATES;
+  config.tryHigherGateLimitForTwoQubitGateOptimization = true;
+  config.useMaxSAT                                     = true;
+  synthesizer.synthesize(config);
+  results = synthesizer.getResults();
+
+  EXPECT_EQ(results.getTwoQubitGates(), test.expectedMinimalTwoQubitGates);
+}
+
+TEST_P(SynthesisTest, TwoQubitGatesMinimalGates) {
+  config.target = TargetMetric::TWO_QUBIT_GATES;
+  config.tryHigherGateLimitForTwoQubitGateOptimization = true;
+  config.minimizeGatesAfterTwoQubitGateOptimization    = true;
+  synthesizer.synthesize(config);
+  results = synthesizer.getResults();
+
+  EXPECT_EQ(results.getTwoQubitGates(), test.expectedMinimalTwoQubitGates);
+  EXPECT_EQ(results.getGates(),
+            test.expectedMinimalGatesAtMinimalTwoQubitGates);
+}
+
+TEST_P(SynthesisTest, TwoQubitGatesMinimalGatesMaxSAT) {
+  config.target = TargetMetric::TWO_QUBIT_GATES;
+  config.tryHigherGateLimitForTwoQubitGateOptimization = true;
+  config.minimizeGatesAfterTwoQubitGateOptimization    = true;
+  config.useMaxSAT                                     = true;
+  synthesizer.synthesize(config);
+  results = synthesizer.getResults();
+
+  EXPECT_EQ(results.getTwoQubitGates(), test.expectedMinimalTwoQubitGates);
+  EXPECT_EQ(results.getGates(),
+            test.expectedMinimalGatesAtMinimalTwoQubitGates);
+}
+
+} // namespace cs
diff --git a/test/python/test_cliffordsynthesis.py b/test/python/test_cliffordsynthesis.py
new file mode 100644
index 000000000..9b187d63f
--- /dev/null
+++ b/test/python/test_cliffordsynthesis.py
@@ -0,0 +1,247 @@
+from __future__ import annotations
+
+import json
+from dataclasses import dataclass
+from pathlib import Path
+
+import pytest
+from mqt import qcec, qmap
+
+from qiskit import QuantumCircuit
+from qiskit.quantum_info import Clifford, PauliList
+
+
+@dataclass
+class Configuration:
+    """Configuration for a test case."""
+
+    expected_minimal_gates: int
+    expected_minimal_depth: int
+    expected_minimal_gates_at_minimal_depth: int
+    expected_minimal_two_qubit_gates: int
+    expected_minimal_gates_at_minimal_two_qubit_gates: int
+
+    description: str
+    initial_tableau: str | None = None
+    target_tableau: str | None = None
+    initial_circuit: str | None = None
+
+
+def create_circuit_tests() -> list[Configuration]:
+    path = Path(__file__).resolve().parent.parent / "cliffordsynthesis" / "circuits.json"
+    with path.open() as f:
+        circuits = json.load(f)
+    return [Configuration(**c) for c in circuits]
+
+
+def create_tableau_tests() -> list[Configuration]:
+    path = Path(__file__).resolve().parent.parent / "cliffordsynthesis" / "tableaus.json"
+    with path.open() as f:
+        tableaus = json.load(f)
+    return [Configuration(**t) for t in tableaus]
+
+
+@pytest.mark.parametrize("test_config", create_circuit_tests())
+@pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"])
+def test_optimize_clifford_gates(test_config: Configuration, use_maxsat: bool) -> None:
+    circ, results = qmap.optimize_clifford(
+        circuit=test_config.initial_circuit, use_maxsat=use_maxsat, target_metric="gates"
+    )
+
+    assert results.gates == test_config.expected_minimal_gates
+    print("\n", circ)
+
+
+@pytest.mark.parametrize("test_config", create_circuit_tests())
+@pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"])
+def test_optimize_clifford_depth(test_config: Configuration, use_maxsat: bool) -> None:
+    circ, results = qmap.optimize_clifford(
+        circuit=test_config.initial_circuit, use_maxsat=use_maxsat, target_metric="depth"
+    )
+
+    assert results.depth == test_config.expected_minimal_depth
+    print("\n", circ)
+
+
+@pytest.mark.parametrize("test_config", create_circuit_tests())
+@pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"])
+def test_optimize_clifford_gates_at_minimal_depth(test_config: Configuration, use_maxsat: bool) -> None:
+    circ, results = qmap.optimize_clifford(
+        circuit=test_config.initial_circuit,
+        use_maxsat=use_maxsat,
+        target_metric="depth",
+        minimize_gates_after_depth_optimization=True,
+    )
+
+    assert results.gates == test_config.expected_minimal_gates_at_minimal_depth
+    print("\n", circ)
+
+
+@pytest.mark.parametrize("test_config", create_circuit_tests())
+@pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"])
+def test_optimize_clifford_two_qubit_gates(test_config: Configuration, use_maxsat: bool) -> None:
+    circ, results = qmap.optimize_clifford(
+        circuit=test_config.initial_circuit,
+        use_maxsat=use_maxsat,
+        target_metric="two_qubit_gates",
+        try_higher_gate_limit_for_two_qubit_gate_optimization=True,
+    )
+
+    assert results.two_qubit_gates == test_config.expected_minimal_two_qubit_gates
+    print("\n", circ)
+
+
+@pytest.mark.parametrize("test_config", create_circuit_tests())
+@pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"])
+def test_optimize_clifford_gates_at_minimal_two_qubit_gates(test_config: Configuration, use_maxsat: bool) -> None:
+    circ, results = qmap.optimize_clifford(
+        circuit=test_config.initial_circuit,
+        use_maxsat=use_maxsat,
+        target_metric="two_qubit_gates",
+        try_higher_gate_limit_for_two_qubit_gate_optimization=True,
+        minimize_gates_after_two_qubit_gate_optimization=True,
+    )
+
+    assert results.gates == test_config.expected_minimal_gates_at_minimal_two_qubit_gates
+    print("\n", circ)
+
+
+@pytest.mark.parametrize("test_config", create_tableau_tests())
+@pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"])
+def test_synthesize_clifford_gates(test_config: Configuration, use_maxsat: bool) -> None:
+    circ, results = qmap.synthesize_clifford(
+        target_tableau=test_config.target_tableau,
+        initial_tableau=test_config.initial_tableau,
+        use_maxsat=use_maxsat,
+        target_metric="gates",
+    )
+
+    assert results.gates == test_config.expected_minimal_gates
+    print("\n", circ)
+
+
+@pytest.mark.parametrize("test_config", create_tableau_tests())
+@pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"])
+def test_synthesize_clifford_depth(test_config: Configuration, use_maxsat: bool) -> None:
+    circ, results = qmap.synthesize_clifford(
+        target_tableau=test_config.target_tableau,
+        initial_tableau=test_config.initial_tableau,
+        use_maxsat=use_maxsat,
+        target_metric="depth",
+    )
+
+    assert results.depth == test_config.expected_minimal_depth
+    print("\n", circ)
+
+
+@pytest.mark.parametrize("test_config", create_tableau_tests())
+@pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"])
+def test_synthesize_clifford_gates_at_minimal_depth(test_config: Configuration, use_maxsat: bool) -> None:
+    circ, results = qmap.synthesize_clifford(
+        target_tableau=test_config.target_tableau,
+        initial_tableau=test_config.initial_tableau,
+        use_maxsat=use_maxsat,
+        target_metric="depth",
+        minimize_gates_after_depth_optimization=True,
+    )
+
+    assert results.gates == test_config.expected_minimal_gates_at_minimal_depth
+    print("\n", circ)
+
+
+@pytest.mark.parametrize("test_config", create_tableau_tests())
+@pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"])
+def test_synthesize_clifford_two_qubit_gates(test_config: Configuration, use_maxsat: bool) -> None:
+    circ, results = qmap.synthesize_clifford(
+        target_tableau=test_config.target_tableau,
+        initial_tableau=test_config.initial_tableau,
+        use_maxsat=use_maxsat,
+        target_metric="two_qubit_gates",
+        try_higher_gate_limit_for_two_qubit_gate_optimization=True,
+    )
+
+    assert results.two_qubit_gates == test_config.expected_minimal_two_qubit_gates
+    print("\n", circ)
+
+
+@pytest.mark.parametrize("test_config", create_tableau_tests())
+@pytest.mark.parametrize("use_maxsat", [True, False], ids=["maxsat", "binary_search"])
+def test_synthesize_clifford_gates_at_minimal_two_qubit_gates(test_config: Configuration, use_maxsat: bool) -> None:
+    circ, results = qmap.synthesize_clifford(
+        target_tableau=test_config.target_tableau,
+        initial_tableau=test_config.initial_tableau,
+        use_maxsat=use_maxsat,
+        target_metric="two_qubit_gates",
+        try_higher_gate_limit_for_two_qubit_gate_optimization=True,
+        minimize_gates_after_two_qubit_gate_optimization=True,
+    )
+
+    assert results.gates == test_config.expected_minimal_gates_at_minimal_two_qubit_gates
+    print("\n", circ)
+
+
+# The following tests merely check that all kinds of conversions work as expected.
+# They only check for the correctness of the result for a simple circuit.
+
+
+@pytest.fixture
+def bell_circuit() -> QuantumCircuit:
+    """Return a Bell state circuit."""
+    circ = QuantumCircuit(2)
+    circ.h(0)
+    circ.cx(0, 1)
+    return circ
+
+
+def test_optimize_quantum_computation(bell_circuit: QuantumCircuit) -> None:
+    """Test that we can optimize an MQT QuantumComputation."""
+    qc = qmap.QuantumComputation.from_qiskit(bell_circuit)
+    circ, results = qmap.optimize_clifford(circuit=qc)
+    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+
+
+def test_optimize_from_qasm_file(bell_circuit: QuantumCircuit) -> None:
+    """Test that we can optimize from a QASM file."""
+    with Path("bell.qasm").open("w") as f:
+        f.write(bell_circuit.qasm())
+    circ, results = qmap.optimize_clifford(circuit="bell.qasm")
+    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+
+
+def test_optimize_qiskit_circuit(bell_circuit: QuantumCircuit) -> None:
+    """Test that we can optimize a Qiskit QuantumCircuit."""
+    circ, results = qmap.optimize_clifford(circuit=bell_circuit)
+    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+
+
+def test_optimize_with_initial_tableau(bell_circuit: QuantumCircuit) -> None:
+    """Test that we can optimize a circuit with an initial tableau."""
+    circ, results = qmap.optimize_clifford(circuit=bell_circuit, initial_tableau=qmap.Tableau(bell_circuit.num_qubits))
+    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+
+
+def test_synthesize_from_tableau(bell_circuit: QuantumCircuit) -> None:
+    """Test that we can synthesize a circuit from an MQT Tableau."""
+    tableau = qmap.Tableau("['XX', 'ZZ']")
+    circ, results = qmap.synthesize_clifford(target_tableau=tableau)
+    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+
+
+def test_synthesize_from_qiskit_clifford(bell_circuit: QuantumCircuit) -> None:
+    """Test that we can synthesize a circuit from a Qiskit Clifford."""
+    cliff = Clifford(bell_circuit)
+    circ, results = qmap.synthesize_clifford(target_tableau=cliff)
+    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+
+
+def test_synthesize_from_qiskit_pauli_list(bell_circuit: QuantumCircuit) -> None:
+    """Test that we can synthesize a circuit from a Qiskit PauliList."""
+    pauli_list = PauliList(["XX", "ZZ"])
+    circ, results = qmap.synthesize_clifford(target_tableau=pauli_list)
+    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+
+
+def test_invalid_kwarg_to_synthesis() -> None:
+    """Test that we raise an error if we pass an invalid kwarg to synthesis."""
+    with pytest.raises(ValueError):
+        qmap.synthesize_clifford(target_tableau=qmap.Tableau("Z"), invalid_kwarg=True)