diff --git a/docs/source/Synthesis.ipynb b/docs/source/Synthesis.ipynb
index 1012b44af..3f54c39ed 100644
--- a/docs/source/Synthesis.ipynb
+++ b/docs/source/Synthesis.ipynb
@@ -286,6 +286,55 @@
     "qc_synth.draw(output=\"mpl\")"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "### Connectivity Constraints on qubits"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "\n",
+    "Limited qubit connectivity is implemented to handle the physical constraints of quantum hardware, where certain qubits can only interact with specific other qubits.\n",
+    "For this a custom coupling map can be passed to the synthesizer, which ensures that the generated circuit from the synthesis respects these connectivity constraints.\n",
+    "The mapping used in the synthesis is also stored in the result returned by the synthesis\n",
+    "\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from qiskit import QuantumCircuit\n",
+    "\n",
+    "from mqt import qmap\n",
+    "\n",
+    "circ = QuantumCircuit(3)\n",
+    "circ.h(1)\n",
+    "circ.h(0)\n",
+    "circ.cx(0, 1)\n",
+    "circ.cx(0, 2)\n",
+    "circ.draw(output=\"mpl\")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "circ_opt, results = qmap.optimize_clifford(circ, coupling_map={(1, 0), (0, 1), (1, 2), (2, 1)})\n",
+    "\n",
+    "print(results.mapping)\n",
+    "print(results.mapping_string)\n",
+    "circ_opt.draw(output=\"mpl\")"
+   ]
+  },
   {
    "cell_type": "markdown",
    "metadata": {},
diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp
index 73ec26eef..088161d65 100644
--- a/include/cliffordsynthesis/CliffordSynthesizer.hpp
+++ b/include/cliffordsynthesis/CliffordSynthesizer.hpp
@@ -12,8 +12,10 @@
 #include "cliffordsynthesis/TargetMetric.hpp"
 #include "cliffordsynthesis/encoding/SATEncoder.hpp"
 #include "ir/QuantumComputation.hpp"
+#include "sc/utils.hpp"
 
 #include <cstddef>
+#include <cstdint>
 #include <limits>
 #include <memory>
 #include <plog/Log.h>
@@ -28,23 +30,49 @@ class CliffordSynthesizer {
 public:
   CliffordSynthesizer() = default;
   CliffordSynthesizer(Tableau initial, Tableau target)
-      : initialTableau(std::move(initial)), targetTableau(std::move(target)) {}
+      : initialTableau(std::move(initial)),
+        couplingMap(getFullyConnectedMap(
+            static_cast<uint16_t>(target.getQubitCount()))),
+        targetTableau(std::move(target)) {}
+  CliffordSynthesizer(Tableau initial, Tableau target, CouplingMap qm)
+      : initialTableau(std::move(initial)), couplingMap(std::move(qm)),
+        targetTableau(std::move(target)) {}
   explicit CliffordSynthesizer(Tableau target)
       : initialTableau(target.getQubitCount(), target.hasDestabilizers()),
+        couplingMap(getFullyConnectedMap(
+            static_cast<uint16_t>(target.getQubitCount()))),
         targetTableau(std::move(target)) {}
   CliffordSynthesizer(Tableau initial, qc::QuantumComputation& qc)
       : initialTableau(std::move(initial)),
+        couplingMap(
+            getFullyConnectedMap(static_cast<uint16_t>(qc.getNqubits()))),
         targetTableau(qc, 0, std::numeric_limits<std::size_t>::max(),
                       initialTableau.hasDestabilizers()),
-        initialCircuit(std::make_shared<qc::QuantumComputation>(qc)),
-        results(qc, targetTableau) {}
+        initialCircuit(std::make_shared<qc::QuantumComputation>(qc)) {}
   explicit CliffordSynthesizer(qc::QuantumComputation& qc,
                                const bool useDestabilizers = false)
       : initialTableau(qc.getNqubits(), useDestabilizers),
+        couplingMap(
+            getFullyConnectedMap(static_cast<uint16_t>(qc.getNqubits()))),
+        targetTableau(qc, 0, std::numeric_limits<std::size_t>::max(),
+                      useDestabilizers),
+        initialCircuit(std::make_shared<qc::QuantumComputation>(qc)) {}
+  explicit CliffordSynthesizer(Tableau target, CouplingMap qm)
+      : initialTableau(target.getQubitCount(), target.hasDestabilizers()),
+        couplingMap(std::move(qm)), targetTableau(std::move(target)) {}
+  CliffordSynthesizer(Tableau initial, qc::QuantumComputation& qc,
+                      CouplingMap qm)
+      : initialTableau(std::move(initial)), couplingMap(std::move(qm)),
+        targetTableau(qc, 0, std::numeric_limits<std::size_t>::max(),
+                      initialTableau.hasDestabilizers()),
+        initialCircuit(std::make_shared<qc::QuantumComputation>(qc)) {}
+  explicit CliffordSynthesizer(qc::QuantumComputation& qc, CouplingMap qm,
+                               const bool useDestabilizers = false)
+      : initialTableau(qc.getNqubits(), useDestabilizers),
+        couplingMap(std::move(qm)),
         targetTableau(qc, 0, std::numeric_limits<std::size_t>::max(),
                       useDestabilizers),
-        initialCircuit(std::make_shared<qc::QuantumComputation>(qc)),
-        results(qc, targetTableau) {}
+        initialCircuit(std::make_shared<qc::QuantumComputation>(qc)) {}
 
   virtual ~CliffordSynthesizer() = default;
 
@@ -72,6 +100,7 @@ class CliffordSynthesizer {
 
 protected:
   Tableau initialTableau;
+  CouplingMap couplingMap;
   Tableau targetTableau;
   std::shared_ptr<qc::QuantumComputation> initialCircuit;
 
diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp
index ed7a6b9f4..3dcfbee12 100644
--- a/include/cliffordsynthesis/Results.hpp
+++ b/include/cliffordsynthesis/Results.hpp
@@ -13,7 +13,10 @@
 #include <limits>
 #include <nlohmann/json_fwd.hpp>
 #include <ostream>
+#include <sstream>
 #include <string>
+#include <utility>
+#include <vector>
 
 namespace cs {
 class Results {
@@ -40,6 +43,20 @@ class Results {
   [[nodiscard]] std::string getResultCircuit() const { return resultCircuit; }
   [[nodiscard]] std::string getResultTableau() const { return resultTableau; }
 
+  [[nodiscard]] std::string getMapping() const {
+    std::ostringstream oss;
+    for (const auto& row : permutationVector) {
+      for (const bool val : row) {
+        oss << (val ? '1' : '0');
+      }
+      oss << '\n';
+    }
+    return oss.str();
+  }
+  [[nodiscard]] std::vector<std::vector<bool>> getMappingVector() const {
+    return permutationVector;
+  }
+
   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; }
@@ -49,6 +66,17 @@ class Results {
 
   void setResultCircuit(qc::QuantumComputation& qc);
   void setResultTableau(const Tableau& tableau);
+  void setMapping(std::vector<std::vector<bool>> p) {
+    std::ostringstream oss;
+    for (const auto& row : permutationVector) {
+      for (const bool val : row) {
+        oss << (val ? '1' : '0');
+      }
+      oss << '\n';
+    }
+    permutationString = oss.str();
+    permutationVector = std::move(p);
+  }
 
   [[nodiscard]] bool sat() const {
     return getSolverResult() == logicbase::Result::SAT;
@@ -69,6 +97,8 @@ class Results {
   double runtime = 0.0;
   std::size_t solverCalls = 0U;
 
+  std::string permutationString;
+  std::vector<std::vector<bool>> permutationVector;
   std::string resultTableau;
   std::string resultCircuit;
 };
diff --git a/include/cliffordsynthesis/Tableau.hpp b/include/cliffordsynthesis/Tableau.hpp
index 77f014a02..226d59e1d 100644
--- a/include/cliffordsynthesis/Tableau.hpp
+++ b/include/cliffordsynthesis/Tableau.hpp
@@ -163,5 +163,10 @@ class Tableau {
   [[nodiscard]] std::uint64_t getBVFrom(const std::size_t column) const {
     return getBVFrom<64>(column).to_ullong();
   }
+  Tableau applyMapping(const std::vector<std::vector<bool>>& p);
+  Tableau reverseMappingOnRows(const std::vector<std::vector<bool>>& p,
+                               size_t nq);
+  void rref();
+  bool equivalentUpToStabilizer(const Tableau* t) const;
 };
 } // namespace cs
diff --git a/include/cliffordsynthesis/encoding/GateEncoder.hpp b/include/cliffordsynthesis/encoding/GateEncoder.hpp
index 923b2c96f..8f3741138 100644
--- a/include/cliffordsynthesis/encoding/GateEncoder.hpp
+++ b/include/cliffordsynthesis/encoding/GateEncoder.hpp
@@ -12,6 +12,7 @@
 #include "logicblocks/Logic.hpp"
 #include "logicblocks/LogicBlock.hpp"
 #include "logicblocks/LogicTerm.hpp"
+#include "sc/utils.hpp"
 
 #include <array>
 #include <cstddef>
@@ -27,8 +28,9 @@ class GateEncoder {
   GateEncoder(const std::size_t nQubits, const std::size_t tableauSize,
               const std::size_t timestepLimit,
               TableauEncoder::Variables* tableauVars,
-              std::shared_ptr<logicbase::LogicBlock> logicBlock)
-      : N(nQubits), S(tableauSize), T(timestepLimit), tvars(tableauVars),
+              std::shared_ptr<logicbase::LogicBlock> logicBlock, CouplingMap cm)
+      : N(nQubits), S(tableauSize), T(timestepLimit),
+        couplingMap(std::move(cm)), tvars(tableauVars),
         lb(std::move(logicBlock)) {}
   virtual ~GateEncoder() = default;
 
@@ -115,6 +117,9 @@ class GateEncoder {
   // timestep limit T
   std::size_t T{}; // NOLINT (readability-identifier-naming)
 
+  // coupling Map
+  CouplingMap couplingMap;
+
   // the gate variables
   Variables vars{};
 
diff --git a/include/cliffordsynthesis/encoding/SATEncoder.hpp b/include/cliffordsynthesis/encoding/SATEncoder.hpp
index b74be864b..950f7f76e 100644
--- a/include/cliffordsynthesis/encoding/SATEncoder.hpp
+++ b/include/cliffordsynthesis/encoding/SATEncoder.hpp
@@ -14,6 +14,7 @@
 #include "cliffordsynthesis/encoding/TableauEncoder.hpp"
 #include "logicblocks/Logic.hpp"
 #include "logicblocks/LogicBlock.hpp"
+#include "sc/utils.hpp"
 
 #include <cstddef>
 #include <memory>
@@ -33,6 +34,9 @@ class SATEncoder {
     // the number of qubits to encode
     std::size_t nQubits{};
 
+    // coupling Map of Qubits
+    CouplingMap couplingMap;
+
     // the number of timesteps to encode
     std::size_t timestepLimit{};
 
diff --git a/include/cliffordsynthesis/encoding/TableauEncoder.hpp b/include/cliffordsynthesis/encoding/TableauEncoder.hpp
index 60c8e947e..c9dc46876 100644
--- a/include/cliffordsynthesis/encoding/TableauEncoder.hpp
+++ b/include/cliffordsynthesis/encoding/TableauEncoder.hpp
@@ -33,6 +33,8 @@ class TableauEncoder {
     logicbase::LogicMatrix z;
     // variables for the phase parts of the tableaus
     logicbase::LogicVector r;
+    // variables for mapping of qubits
+    logicbase::LogicMatrix p;
 
     // update rules for single-qubit gates
     [[nodiscard]] logicbase::LogicTerm
@@ -58,7 +60,7 @@ class TableauEncoder {
   void createTableauVariables();
 
   // fixing the tableau
-  void assertTableau(const Tableau& tableau, std::size_t t);
+  void assertTableau(const Tableau& tableau, std::size_t t) const;
 
   // extracting the tableau
   void extractTableauFromModel(Results& results, std::size_t t,
@@ -66,6 +68,12 @@ class TableauEncoder {
 
   [[nodiscard]] auto* getVariables() { return &vars; }
 
+  // get mapping variables and store them in results
+  void extractMappingFromModel(Results& results, logicbase::Model& model) const;
+
+  // assert constraints for mapping variables
+  void assertMappingConstraints() const;
+
 protected:
   // number of qubits N
   std::size_t N{}; // NOLINT (readability-identifier-naming)
diff --git a/src/cliffordsynthesis/CMakeLists.txt b/src/cliffordsynthesis/CMakeLists.txt
index 832ec3f11..977e7303d 100644
--- a/src/cliffordsynthesis/CMakeLists.txt
+++ b/src/cliffordsynthesis/CMakeLists.txt
@@ -10,11 +10,12 @@ if(NOT TARGET ${MQT_QMAP_CLIFFORD_SYNTHESIS_TARGET_NAME})
   file(GLOB_RECURSE CLIFFORD_SYNTHESIS_HEADERS
        ${MQT_QMAP_INCLUDE_BUILD_DIR}/cliffordsynthesis/*.hpp)
   file(GLOB_RECURSE CLIFFORD_SYNTHESIS_SOURCES **.cpp)
+  list(APPEND CLIFFORD_SYNTHESIS_SOURCES "${CMAKE_SOURCE_DIR}/src/sc/utils.cpp")
 
   # add CliffordSynthesis Package library
   add_library(${MQT_QMAP_CLIFFORD_SYNTHESIS_TARGET_NAME} ${CLIFFORD_SYNTHESIS_HEADERS}
                                                          ${CLIFFORD_SYNTHESIS_SOURCES})
-
+  message(${CLIFFORD_SYNTHESIS_SOURCES})
   # set include directories
   target_include_directories(${MQT_QMAP_CLIFFORD_SYNTHESIS_TARGET_NAME}
                              PUBLIC $<BUILD_INTERFACE:${MQT_QMAP_INCLUDE_BUILD_DIR}>)
diff --git a/src/cliffordsynthesis/CliffordSynthesizer.cpp b/src/cliffordsynthesis/CliffordSynthesizer.cpp
index cd9d7416d..e78603e19 100644
--- a/src/cliffordsynthesis/CliffordSynthesizer.cpp
+++ b/src/cliffordsynthesis/CliffordSynthesizer.cpp
@@ -6,6 +6,7 @@
 #include "cliffordsynthesis/CliffordSynthesizer.hpp"
 
 #include "cliffordsynthesis/Configuration.hpp"
+#include "cliffordsynthesis/Results.hpp"
 #include "cliffordsynthesis/Tableau.hpp"
 #include "cliffordsynthesis/TargetMetric.hpp"
 #include "cliffordsynthesis/encoding/SATEncoder.hpp"
@@ -52,6 +53,7 @@ void CliffordSynthesizer::synthesize(const Configuration& config) {
   encoderConfig.initialTableau = &initialTableau;
   encoderConfig.targetTableau = &targetTableau;
   encoderConfig.nQubits = initialTableau.getQubitCount();
+  encoderConfig.couplingMap = couplingMap;
   encoderConfig.timestepLimit = configuration.initialTimestepLimit;
   encoderConfig.targetMetric = configuration.target;
   encoderConfig.useMaxSAT = configuration.useMaxSAT;
@@ -85,6 +87,7 @@ void CliffordSynthesizer::synthesize(const Configuration& config) {
     const auto [lowerBin, upperBin] = determineUpperBound(encoderConfig);
     lower = lowerBin;
     upper = upperBin;
+    PLOG_INFO << "Upper bound " << upperBin;
 
     // if the upper bound is 0, the solution does not require any gates and the
     // synthesis is done.
@@ -95,7 +98,10 @@ void CliffordSynthesizer::synthesize(const Configuration& config) {
   }
   // Otherwise, the determined upper bound is used as an initial timestep
   // limit.
+
   encoderConfig.timestepLimit = upper;
+  PLOG_INFO << "Upper bound " << encoderConfig.timestepLimit;
+
   // Once a valid upper bound is found, the SAT problem is solved again with
   // the objective function encoded.
   switch (config.target) {
@@ -491,6 +497,7 @@ std::vector<std::size_t> getLayers(const qc::QuantumComputation& qc) {
 void CliffordSynthesizer::depthHeuristicSynthesis() {
   PLOG_INFO << "Optimizing Circuit with Heuristic";
   if (initialCircuit->getDepth() == 0) {
+    results.setResultCircuit(*initialCircuit);
     return;
   }
   auto optimalConfig = configuration;
diff --git a/src/cliffordsynthesis/Tableau.cpp b/src/cliffordsynthesis/Tableau.cpp
index 0f4b83537..98e51eeb4 100644
--- a/src/cliffordsynthesis/Tableau.cpp
+++ b/src/cliffordsynthesis/Tableau.cpp
@@ -525,4 +525,104 @@ bool Tableau::isIdentityTableau() const {
   }
   return true;
 }
+
+Tableau Tableau::applyMapping(const std::vector<std::vector<bool>>& p) {
+  Tableau mappedTableau = Tableau(nQubits, hasDestabilizers());
+  for (size_t i = 0; i < p.size(); i++) {
+    for (size_t j = 0; j < p[i].size(); j++) {
+      // apply mapping from column i to j if p is set
+      if (p[i][j]) {
+        // in every row swap x entry and z entry
+        for (size_t n = 0; n < mappedTableau.getTableauSize(); n++) {
+          mappedTableau.tableau[n][j] = tableau[n][i];
+          mappedTableau.tableau[n][j + mappedTableau.nQubits] =
+              tableau[n][i + mappedTableau.nQubits];
+        }
+      }
+    }
+  }
+  // copy r column without changes
+  for (size_t i = 0; i < tableau.size(); i++) {
+    mappedTableau.tableau[i][2 * nQubits] = tableau[i][2 * nQubits];
+  }
+  return mappedTableau;
+}
+
+// number of Qubits is passed because nQubits is not set in result Tableau of
+// synthesis
+Tableau Tableau::reverseMappingOnRows(const std::vector<std::vector<bool>>& p,
+                                      const size_t nq) {
+  auto mappedTableau = Tableau(nq, true);
+  mappedTableau.tableau = tableau;
+  for (size_t i = 0; i < p.size(); i++) {
+    for (size_t j = 0; j < p[i].size(); j++) {
+      // apply mapping from row i to j if p is set
+      if (p[i][j]) {
+        mappedTableau.tableau[i] = tableau[j];
+        mappedTableau.tableau[i + nq] = tableau[j + nq];
+      }
+    }
+  }
+  return mappedTableau;
+}
+
+// in place Gauss Elimination
+void Tableau::rref() {
+  const size_t rows = tableau.size();
+  const size_t cols = tableau[0].size();
+  if (rows == 1) {
+    return;
+  }
+
+  size_t pivot = 0;
+
+  for (size_t col = 0; col < cols; ++col) {
+    // find the pivot row for the current column
+    size_t maxRow = pivot;
+    if (maxRow >= rows) {
+      break;
+    }
+    for (size_t row = pivot; row < rows; ++row) {
+      if (tableau[row][col] == 1) {
+        maxRow = row;
+        break;
+      }
+    }
+    // if no pivot is found, continue to the next column
+    if (tableau[maxRow][col] == 0) {
+      continue;
+    }
+    // swap the pivot row with the current row
+    std::swap(tableau[pivot], tableau[maxRow]);
+
+    // eliminate all other 1s in the current column
+    for (size_t row = 0; row < rows; ++row) {
+      if (row != pivot && tableau[row][col] == 1) {
+        for (size_t k = 0; k < cols; ++k) {
+          if (tableau[row][k] == tableau[pivot][k]) {
+            tableau[row][k] = 0;
+          } else {
+            tableau[row][k] = 1;
+          }
+        }
+      }
+    }
+    pivot++;
+  }
+}
+// equivalence check for two Tableaus without destablilizers
+bool Tableau::equivalentUpToStabilizer(const Tableau* t) const {
+  if (getTableauSize() != t->getTableauSize()) {
+    return false;
+  }
+
+  Tableau tEliminated = Tableau(nQubits, hasDestabilizers());
+  tEliminated.tableau = tableau;
+  tEliminated.rref();
+
+  Tableau t2Eliminated = Tableau(nQubits, hasDestabilizers());
+  t2Eliminated.tableau = t->getTableau();
+  t2Eliminated.rref();
+  return tEliminated == t2Eliminated;
+}
 } // namespace cs
diff --git a/src/cliffordsynthesis/encoding/GateEncoder.cpp b/src/cliffordsynthesis/encoding/GateEncoder.cpp
index 958277e98..2634ac5fa 100644
--- a/src/cliffordsynthesis/encoding/GateEncoder.cpp
+++ b/src/cliffordsynthesis/encoding/GateEncoder.cpp
@@ -14,6 +14,7 @@
 #include "ir/operations/StandardOperation.hpp"
 #include "logicblocks/Encodings.hpp"
 #include "logicblocks/Model.hpp"
+#include "sc/utils.hpp"
 
 #include <algorithm>
 #include <cstddef>
@@ -135,12 +136,12 @@ void GateEncoder::assertZConstraints(const std::size_t pos,
                                      const std::size_t qubit) {
   const auto& gatesToZTransformations = [this](const auto& p1, const auto& p2,
                                                const auto& p3) {
-    return tvars->singleQubitZChange(p1, p2, p3);
+    return tvars->singleQubitZChange(p1 + 1, p2, p3);
   };
   auto gateTransformations =
       collectGateTransformations(pos, qubit, gatesToZTransformations);
   for (auto& [transformation, _] : gateTransformations) {
-    transformation = tvars->z[pos + 1][qubit] == transformation;
+    transformation = tvars->z[pos + 2][qubit] == transformation;
   }
   assertGatesImplyTransform(pos, qubit, gateTransformations);
 }
@@ -149,12 +150,12 @@ void GateEncoder::assertXConstraints(const std::size_t pos,
                                      const std::size_t qubit) {
   const auto& gatesToXTransformations = [this](const auto& p1, const auto& p2,
                                                const auto& p3) {
-    return tvars->singleQubitXChange(p1, p2, p3);
+    return tvars->singleQubitXChange(p1 + 1, p2, p3);
   };
   auto gateTransformations =
       collectGateTransformations(pos, qubit, gatesToXTransformations);
   for (auto& [transformation, _] : gateTransformations) {
-    transformation = tvars->x[pos + 1][qubit] == transformation;
+    transformation = tvars->x[pos + 2][qubit] == transformation;
   }
   assertGatesImplyTransform(pos, qubit, gateTransformations);
 }
@@ -163,12 +164,12 @@ void GateEncoder::assertRConstraints(const std::size_t pos,
                                      const std::size_t qubit) {
   const auto& gatesToRTransformations = [this](const auto& p1, const auto& p2,
                                                const auto& p3) {
-    return tvars->singleQubitRChange(p1, p2, p3);
+    return tvars->singleQubitRChange(p1 + 1, p2, p3);
   };
   auto gateTransformations =
       collectGateTransformations(pos, qubit, gatesToRTransformations);
   for (auto& [transformation, _] : gateTransformations) {
-    transformation = tvars->r[pos + 1] == (tvars->r[pos] ^ transformation);
+    transformation = tvars->r[pos + 2] == (tvars->r[pos + 1] ^ transformation);
   }
   assertGatesImplyTransform(pos, qubit, gateTransformations);
 }
@@ -346,6 +347,10 @@ void GateEncoder::assertTwoQubitGateSymmetryBreakingConstraints(
     const std::size_t pos) {
   for (std::size_t ctrl = 1U; ctrl < N; ++ctrl) {
     for (std::size_t trgt = 0U; trgt < ctrl; ++trgt) {
+      // avoid unnecessary constraints if CNOT cannot be applied anyways
+      if (couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) {
+        continue;
+      }
       assertTwoQubitGateOrderConstraints(pos, ctrl, trgt);
     }
   }
diff --git a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp
index b2d8d4f33..6f4fa48f8 100644
--- a/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp
+++ b/src/cliffordsynthesis/encoding/MultiGateEncoder.cpp
@@ -8,6 +8,7 @@
 #include "Logic.hpp"
 #include "ir/operations/OpType.hpp"
 #include "logicblocks/LogicTerm.hpp"
+#include "sc/utils.hpp"
 
 #include <cstddef>
 #include <cstdint>
@@ -46,12 +47,12 @@ void encoding::MultiGateEncoder::assertGateConstraints() {
   xorHelpers = logicbase::LogicMatrix{T};
   for (std::size_t t = 0U; t < T; ++t) {
     PLOG_VERBOSE << "Asserting gate constraints at time " << t;
-    rChanges = tvars->r[t];
-    splitXorR(tvars->r[t], t);
+    rChanges = tvars->r[t + 1];
+    splitXorR(tvars->r[t + 1], t);
     assertSingleQubitGateConstraints(t);
     assertTwoQubitGateConstraints(t);
     PLOG_VERBOSE << "Asserting r changes at time " << t;
-    lb->assertFormula(tvars->r[t + 1] == xorHelpers[t].back());
+    lb->assertFormula(tvars->r[t + 2] == xorHelpers[t].back());
   }
 }
 
@@ -69,7 +70,7 @@ void MultiGateEncoder::assertRConstraints(const std::size_t pos,
   for (const auto gate : SINGLE_QUBIT_GATES) {
     const auto& change =
         LogicTerm::ite(vars.gS[pos][gateToIndex(gate)][qubit],
-                       tvars->singleQubitRChange(pos, qubit, gate),
+                       tvars->singleQubitRChange(pos + 1, qubit, gate),
                        LogicTerm(0, static_cast<std::uint16_t>(S)));
     splitXorR(change, pos);
   }
@@ -83,6 +84,12 @@ void encoding::MultiGateEncoder::assertTwoQubitGateConstraints(
       if (ctrl == trgt) {
         continue;
       }
+      // if no connection between ctrl and trgt then assert variable is false
+      if (couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) {
+        PLOG_DEBUG << "Asserting no CNOT on " << ctrl << " and " << trgt;
+        lb->assertFormula(!twoQubitGates[ctrl][trgt]);
+        continue;
+      }
       const auto changes = createTwoQubitGateConstraint(pos, ctrl, trgt);
       lb->assertFormula(LogicTerm::implies(twoQubitGates[ctrl][trgt], changes));
 
@@ -94,16 +101,16 @@ void encoding::MultiGateEncoder::assertTwoQubitGateConstraints(
 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);
+  const auto [xCtrl, xTrgt] = tvars->twoQubitXChange(pos + 1, ctrl, trgt);
+  const auto [zCtrl, zTrgt] = tvars->twoQubitZChange(pos + 1, 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->x[pos + 2][ctrl] == xCtrl);
+  changes = changes && (tvars->x[pos + 2][trgt] == xTrgt);
+  changes = changes && (tvars->z[pos + 2][ctrl] == zCtrl);
+  changes = changes && (tvars->z[pos + 2][trgt] == zTrgt);
 
   const auto& newRChanges = LogicTerm::ite(
-      vars.gC[pos][ctrl][trgt], tvars->twoQubitRChange(pos, ctrl, trgt),
+      vars.gC[pos][ctrl][trgt], tvars->twoQubitRChange(pos + 1, ctrl, trgt),
       LogicTerm(0, static_cast<std::uint16_t>(S)));
   splitXorR(newRChanges, pos);
   return changes;
diff --git a/src/cliffordsynthesis/encoding/SATEncoder.cpp b/src/cliffordsynthesis/encoding/SATEncoder.cpp
index a702f52b2..6e2249fd5 100644
--- a/src/cliffordsynthesis/encoding/SATEncoder.cpp
+++ b/src/cliffordsynthesis/encoding/SATEncoder.cpp
@@ -69,17 +69,18 @@ void SATEncoder::createFormulation() {
                             ? 2U * N
                             : N;
 
-  tableauEncoder = std::make_shared<TableauEncoder>(N, s, T, lb);
+  tableauEncoder = std::make_shared<TableauEncoder>(N, s, T + 2, lb);
   tableauEncoder->createTableauVariables();
   tableauEncoder->assertTableau(*config.initialTableau, 0U);
-  tableauEncoder->assertTableau(*config.targetTableau, T);
+  tableauEncoder->assertTableau(*config.targetTableau, T + 2);
+  tableauEncoder->assertMappingConstraints();
 
   if (config.useMultiGateEncoding) {
     gateEncoder = std::make_shared<MultiGateEncoder>(
-        N, s, T, tableauEncoder->getVariables(), lb);
+        N, s, T, tableauEncoder->getVariables(), lb, config.couplingMap);
   } else {
     gateEncoder = std::make_shared<SingleGateEncoder>(
-        N, s, T, tableauEncoder->getVariables(), lb);
+        N, s, T, tableauEncoder->getVariables(), lb, config.couplingMap);
   }
   gateEncoder->createSingleQubitGateVariables();
   gateEncoder->createTwoQubitGateVariables();
@@ -127,7 +128,9 @@ Result SATEncoder::solve() const {
 
 void SATEncoder::extractResultsFromModel(Results& res) const {
   auto* const model = lb->getModel();
-  tableauEncoder->extractTableauFromModel(res, T, *model);
+  // result is tableau with mapping applied
+  tableauEncoder->extractTableauFromModel(res, T + 1, *model);
+  tableauEncoder->extractMappingFromModel(res, *model);
   gateEncoder->extractCircuitFromModel(res, *model);
 }
 
diff --git a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp
index f016108e8..2c2280e3a 100644
--- a/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp
+++ b/src/cliffordsynthesis/encoding/SingleGateEncoder.cpp
@@ -7,6 +7,7 @@
 
 #include "Logic.hpp"
 #include "ir/operations/OpType.hpp"
+#include "sc/utils.hpp"
 
 #include <cstddef>
 #include <plog/Log.h>
@@ -71,6 +72,11 @@ void SingleGateEncoder::assertTwoQubitGateConstraints(const std::size_t pos) {
       if (ctrl == trgt) {
         continue;
       }
+      if (couplingMap.find(Edge{ctrl, trgt}) == couplingMap.end()) {
+        PLOG_DEBUG << "Asserting no CNOT on " << ctrl << " and " << trgt;
+        lb->assertFormula(!twoQubitGates[ctrl][trgt]);
+        continue;
+      }
       const auto changes = createTwoQubitGateConstraint(pos, ctrl, trgt);
 
       PLOG_DEBUG << "Asserting CNOT on " << ctrl << " and " << trgt;
@@ -83,16 +89,16 @@ void SingleGateEncoder::assertTwoQubitGateConstraints(const std::size_t pos) {
 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);
+  const auto [xCtrl, xTrgt] = tvars->twoQubitXChange(pos + 1, ctrl, trgt);
+  const auto [zCtrl, zTrgt] = tvars->twoQubitZChange(pos + 1, 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)));
+  changes = changes && (tvars->x[pos + 2][ctrl] == xCtrl);
+  changes = changes && (tvars->x[pos + 2][trgt] == xTrgt);
+  changes = changes && (tvars->z[pos + 2][ctrl] == zCtrl);
+  changes = changes && (tvars->z[pos + 2][trgt] == zTrgt);
+  changes = changes &&
+            (tvars->r[pos + 2] ==
+             (tvars->r[pos + 1] ^ tvars->twoQubitRChange(pos + 1, ctrl, trgt)));
 
   return changes;
 }
@@ -100,8 +106,8 @@ LogicTerm SingleGateEncoder::createTwoQubitGateConstraint(
 LogicTerm SingleGateEncoder::createNoChangeOnQubit(const std::size_t pos,
                                                    const std::size_t q) {
   auto noChange = LogicTerm(true);
-  noChange = noChange && (tvars->x[pos + 1][q] == tvars->x[pos][q]);
-  noChange = noChange && (tvars->z[pos + 1][q] == tvars->z[pos][q]);
+  noChange = noChange && (tvars->x[pos + 2][q] == tvars->x[pos + 1][q]);
+  noChange = noChange && (tvars->z[pos + 2][q] == tvars->z[pos + 1][q]);
   return noChange;
 }
 
diff --git a/src/cliffordsynthesis/encoding/TableauEncoder.cpp b/src/cliffordsynthesis/encoding/TableauEncoder.cpp
index fb8848bd7..864a136ee 100644
--- a/src/cliffordsynthesis/encoding/TableauEncoder.cpp
+++ b/src/cliffordsynthesis/encoding/TableauEncoder.cpp
@@ -6,9 +6,11 @@
 #include "cliffordsynthesis/encoding/TableauEncoder.hpp"
 
 #include "Logic.hpp"
+#include "LogicTerm.hpp"
 #include "cliffordsynthesis/Results.hpp"
 #include "cliffordsynthesis/Tableau.hpp"
 #include "ir/operations/OpType.hpp"
+#include "logicblocks/Encodings.hpp"
 #include "logicblocks/Model.hpp"
 
 #include <cstddef>
@@ -17,6 +19,7 @@
 #include <stdexcept>
 #include <string>
 #include <utility>
+#include <vector>
 
 namespace cs::encoding {
 
@@ -48,10 +51,22 @@ void TableauEncoder::createTableauVariables() {
     PLOG_VERBOSE << "Creating variable " << rName;
     vars.r.emplace_back(lb->makeVariable(rName, CType::BITVECTOR, n));
   }
+  PLOG_DEBUG << "Creating mapping variables.";
+  vars.p.reserve(N);
+  for (std::size_t i = 0U; i < N; ++i) {
+    auto& g = vars.p.emplace_back();
+    g.reserve(N);
+    for (std::size_t j = 0U; j < N; ++j) {
+      const std::string pName =
+          "p_" + std::to_string(i) + "_" + std::to_string(j);
+      PLOG_VERBOSE << "Creating variable " << pName;
+      g.emplace_back(lb->makeVariable(pName));
+    }
+  }
 }
 
 void TableauEncoder::assertTableau(const Tableau& tableau,
-                                   const std::size_t t) {
+                                   const std::size_t t) const {
   const auto n = static_cast<std::uint16_t>(S);
 
   PLOG_DEBUG << "Asserting tableau at time step " << t;
@@ -68,6 +83,48 @@ void TableauEncoder::assertTableau(const Tableau& tableau,
   lb->assertFormula(vars.r[t] == LogicTerm(targetR, n));
 }
 
+void TableauEncoder::assertMappingConstraints() const {
+  // if p_i_j is set column i is mapped to column j between 0 and 1
+  for (std::size_t i = 0U; i < N; ++i) {
+    for (std::size_t j = 0U; j < N; ++j) {
+      lb->assertFormula(
+          LogicTerm::implies(vars.p[i][j], vars.x[1][j] == vars.x[0][i]));
+      lb->assertFormula(
+          LogicTerm::implies(vars.p[i][j], vars.z[1][j] == vars.z[0][i]));
+    }
+  }
+  // assert that r vals are unchanges between 0 and 1
+  lb->assertFormula(LogicTerm::eq(vars.r[0], vars.r[1]));
+
+  // assert that for every i and j exactly one p variable is set
+  for (std::size_t i = 0U; i < N; ++i) {
+    std::vector<encodings::NestedVar> rowVars;
+    for (std::size_t j = 0U; j < N; ++j) {
+      rowVars.emplace_back(vars.p[i][j]);
+    }
+    lb->assertFormula(
+        encodings::exactlyOneCmdr(rowVars, LogicTerm::noneTerm(), lb.get()));
+
+    std::vector<encodings::NestedVar> colVars;
+    for (std::size_t j = 0U; j < N; ++j) {
+      colVars.emplace_back(vars.p[j][i]);
+    }
+    lb->assertFormula(
+        encodings::exactlyOneCmdr(colVars, LogicTerm::noneTerm(), lb.get()));
+  }
+  // if p_i_j is set undo mapping between T-1 and T
+  for (std::size_t i = 0U; i < N; ++i) {
+    for (std::size_t j = 0U; j < N; ++j) {
+      lb->assertFormula(
+          LogicTerm::implies(vars.p[i][j], vars.x[T][i] == vars.x[T - 1][j]));
+      lb->assertFormula(
+          LogicTerm::implies(vars.p[i][j], vars.z[T][i] == vars.z[T - 1][j]));
+    }
+  }
+  // assert that r vals are unchanges between T-1 and T
+  lb->assertFormula(LogicTerm::eq(vars.r[T - 1], vars.r[T]));
+}
+
 void TableauEncoder::extractTableauFromModel(Results& results,
                                              const std::size_t t,
                                              Model& model) const {
@@ -84,6 +141,19 @@ void TableauEncoder::extractTableauFromModel(Results& results,
   results.setResultTableau(tableau);
 }
 
+void TableauEncoder::extractMappingFromModel(Results& results,
+                                             Model& model) const {
+  const std::vector<bool> row(N, false);
+  std::vector<std::vector<bool>> permutationValues(N,
+                                                   std::vector<bool>(N, false));
+  for (std::size_t i = 0; i < N; ++i) {
+    for (std::size_t j = 0; j < N; ++j) {
+      permutationValues[i][j] = model.getBoolValue(vars.p[i][j], lb.get());
+    }
+  }
+  results.setMapping(permutationValues);
+}
+
 LogicTerm
 TableauEncoder::Variables::singleQubitXChange(const std::size_t pos,
                                               const std::size_t qubit,
diff --git a/src/mqt/qmap/clifford_synthesis.py b/src/mqt/qmap/clifford_synthesis.py
index 444d32afb..935c0e67d 100644
--- a/src/mqt/qmap/clifford_synthesis.py
+++ b/src/mqt/qmap/clifford_synthesis.py
@@ -2,7 +2,7 @@
 
 from __future__ import annotations
 
-from typing import Any
+from typing import TYPE_CHECKING, Any
 
 from qiskit import QuantumCircuit, qasm3
 from qiskit.quantum_info import Clifford, PauliList
@@ -17,6 +17,9 @@
     Tableau,
 )
 
+if TYPE_CHECKING:
+    from collections.abc import Iterable
+
 
 def _import_circuit(circuit: str | QuantumCircuit | QuantumComputation) -> QuantumComputation:
     """Import a circuit from a string, a QuantumCircuit, or a QuantumComputation."""
@@ -37,18 +40,10 @@ def _import_tableau(tableau: str | Clifford | PauliList | Tableau, include_desta
     """Import a tableau from a string, a Clifford, a PauliList, or a Tableau."""
     if isinstance(tableau, Clifford):
         mode = "B" if include_destabilizers else "S"
-        try:
-            return Tableau(str(_reverse_paulis(tableau.to_labels(mode=mode))))
-        except AttributeError:
-            if include_destabilizers:
-                return Tableau(
-                    str(_reverse_paulis(tableau.stabilizer.to_labels())),
-                    str(_reverse_paulis(tableau.destabilizer.to_labels())),
-                )
-            return Tableau(str(_reverse_paulis(tableau.stabilizer.to_labels())))
-    elif isinstance(tableau, PauliList):
+        return Tableau(str(_reverse_paulis(tableau.to_labels(mode=mode))))
+    if isinstance(tableau, PauliList):
         return Tableau(str(_reverse_paulis(tableau.to_labels())))
-    elif isinstance(tableau, str):
+    if isinstance(tableau, str):
         return Tableau(tableau)
     return tableau
 
@@ -96,6 +91,7 @@ def synthesize_clifford(
     target_tableau: str | Clifford | PauliList | Tableau,
     initial_tableau: str | Clifford | PauliList | Tableau | None = None,
     include_destabilizers: bool = False,
+    coupling_map: Iterable[tuple[int, int]] | None = None,
     **kwargs: Any,  # noqa: ANN401
 ) -> tuple[QuantumCircuit, SynthesisResults]:
     """Synthesize a Clifford circuit from a given tableau starting from an (optional) initial tableau.
@@ -114,6 +110,8 @@ def synthesize_clifford(
             If no initial tableau is given, the synthesis starts from the identity tableau.
         include_destabilizers:
             Flag to set whether destabilizers should be considered in the synthesis
+        coupling_map:
+             Iterable of tuples of connected qubits of the architecture to synthesize for.
         **kwargs:
             Additional keyword arguments to configure the synthesis.
             See :class:`SynthesisConfiguration` for a list of available options.
@@ -125,7 +123,12 @@ def synthesize_clifford(
 
     tableau = _import_tableau(target_tableau, include_destabilizers)
     if initial_tableau is not None:
-        synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau), tableau)
+        if coupling_map is not None:
+            synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau), tableau, set(coupling_map))
+        else:
+            synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau), tableau)
+    elif coupling_map is not None:
+        synthesizer = CliffordSynthesizer(tableau, set(coupling_map))
     else:
         synthesizer = CliffordSynthesizer(tableau)
 
@@ -141,6 +144,7 @@ def optimize_clifford(
     circuit: str | QuantumCircuit | QuantumComputation,
     initial_tableau: str | Clifford | PauliList | Tableau | None = None,
     include_destabilizers: bool = False,
+    coupling_map: Iterable[tuple[int, int]] | None = None,
     **kwargs: Any,  # noqa: ANN401
 ) -> tuple[QuantumCircuit, SynthesisResults]:
     """Optimize a Clifford circuit starting from an (optional) initial tableau.
@@ -159,6 +163,8 @@ def optimize_clifford(
             If no initial tableau is given, the synthesis starts from the identity tableau.
         include_destabilizers:
             Flag to set whether destabilizers should be considered in the synthesis
+        coupling_map:
+            Iterable of tuples of connected qubits of the architecture to synthesize for.
         **kwargs:
             Additional keyword arguments to configure the synthesis.
             See :class:`SynthesisConfiguration` for a list of available options.
@@ -170,7 +176,14 @@ def optimize_clifford(
 
     qc = _import_circuit(circuit)
     if initial_tableau is not None:
-        synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau, include_destabilizers), qc)
+        if coupling_map is not None:
+            synthesizer = CliffordSynthesizer(
+                _import_tableau(initial_tableau, include_destabilizers), qc, set(coupling_map)
+            )
+        else:
+            synthesizer = CliffordSynthesizer(_import_tableau(initial_tableau, include_destabilizers), qc)
+    elif coupling_map is not None:
+        synthesizer = CliffordSynthesizer(qc, set(coupling_map), include_destabilizers)
     else:
         synthesizer = CliffordSynthesizer(qc, include_destabilizers)
 
diff --git a/src/mqt/qmap/pyqmap.pyi b/src/mqt/qmap/pyqmap.pyi
index 34efe68bb..e9b2d046e 100644
--- a/src/mqt/qmap/pyqmap.pyi
+++ b/src/mqt/qmap/pyqmap.pyi
@@ -487,6 +487,10 @@ class SynthesisResults:
     def tableau(self) -> str: ...
     @property
     def two_qubit_gates(self) -> int: ...
+    @property
+    def mapping(self) -> list[list[bool]]: ...
+    @property
+    def mapping_string(self) -> str: ...
 
 class QuantumComputation:
     def __init__(self) -> None: ...
@@ -514,6 +518,18 @@ class CliffordSynthesizer:
     def __init__(self, qc: QuantumComputation, use_destabilizers: bool) -> None: ...
     @overload
     def __init__(self, initial_tableau: Tableau, qc: QuantumComputation) -> None: ...
+    @overload
+    def __init__(
+        self, initial_tableau: Tableau, target_tableau: Tableau, coupling_map: set[tuple[int, int]]
+    ) -> None: ...
+    @overload
+    def __init__(self, target_tableau: Tableau, coupling_map: set[tuple[int, int]]) -> None: ...
+    @overload
+    def __init__(self, qc: QuantumComputation, coupling_map: set[tuple[int, int]], use_destabilizers: bool) -> None: ...
+    @overload
+    def __init__(
+        self, initial_tableau: Tableau, qc: QuantumComputation, coupling_map: set[tuple[int, int]]
+    ) -> None: ...
     def synthesize(self, config: SynthesisConfiguration = ...) -> None: ...
     @property
     def results(self) -> SynthesisResults: ...
diff --git a/src/python/bindings.cpp b/src/python/bindings.cpp
index dc87016d4..e5b166db1 100644
--- a/src/python/bindings.cpp
+++ b/src/python/bindings.cpp
@@ -640,6 +640,11 @@ PYBIND11_MODULE(pyqmap, m, py::mod_gil_not_used()) {
       .def_property_readonly("tableau", &cs::Results::getResultTableau,
                              "Returns a string representation of the "
                              "synthesized circuit's tableau.")
+      .def_property_readonly(
+          "mapping", &cs::Results::getMappingVector,
+          "Returns a vector of vectors representing the mapping.")
+      .def_property_readonly("mapping_string", &cs::Results::getMapping,
+                             "Returns a string representation of the mapping.")
       .def("sat", &cs::Results::sat,
            "Returns `true` if the synthesis was successful.")
       .def("unsat", &cs::Results::unsat,
@@ -708,6 +713,28 @@ PYBIND11_MODULE(pyqmap, m, py::mod_gil_not_used()) {
       "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(py::init<cs::Tableau, cs::Tableau, CouplingMap>(),
+                  "initial_tableau"_a, "target_tableau"_a, "coupling_map"_a,
+                  "Constructs a synthesizer for two tableaus representing the "
+                  "initial and target state with a coupling map.");
+
+  synthesizer.def(py::init<cs::Tableau, CouplingMap>(), "target_tableau"_a,
+                  "coupling_map"_a,
+                  "Constructs a synthesizer for a tableau representing the "
+                  "target state with a coupling map.");
+
+  synthesizer.def(py::init<qc::QuantumComputation&, CouplingMap, bool>(),
+                  "qc"_a, "coupling_map"_a,
+                  "use_destabilizers"_a
+                  "Constructs a synthesizer for a quantum computation "
+                  "representing the target state with a coupling map.");
+
+  synthesizer.def(
+      py::init<cs::Tableau, qc::QuantumComputation&, CouplingMap>(),
+      "initial_tableau"_a, "qc"_a, "coupling_map"_a,
+      "Constructs a synthesizer for a quantum computation representing the "
+      "target state that starts in an initial state represented by a tableau "
+      "with a coupling map.");
   synthesizer.def("synthesize", &cs::CliffordSynthesizer::synthesize,
                   "config"_a = cs::Configuration(),
                   "Runs the synthesis with the given configuration.");
diff --git a/test/cliffordsynthesis/circuits.json b/test/cliffordsynthesis/circuits.json
index 00fb48e24..ff06a1b13 100644
--- a/test/cliffordsynthesis/circuits.json
+++ b/test/cliffordsynthesis/circuits.json
@@ -43,5 +43,95 @@
     "expected_minimal_gates_at_minimal_depth": 2,
     "expected_minimal_two_qubit_gates": 0,
     "expected_minimal_gates_at_minimal_two_qubit_gates": 2
+  },
+  {
+    "description": "cx_coupling_test",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[3];h q[1]; cx q[1], q[0]; cx q[1], q[2];\n",
+    "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,
+    "coupling_map": "{0,1};{1,0};{1,2};{2,1}"
+  },
+  {
+    "description": "cx_coupling_test_init_1_final_2",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[3];h q[1]; cx q[1], q[0]; cx q[1], q[2];\n",
+    "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,
+    "coupling_map": "{0,2};{2,0};{1,2};{2,1}"
+  },
+  {
+    "description": "cx_coupling_test_init_1_final_0",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[3];h q[1]; cx q[1], q[0]; cx q[1], q[2];\n",
+    "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,
+    "coupling_map": "{0,2};{2,0};{1,0};{0,1}"
+  },
+  {
+    "description": "cx_coupling_test_init_2_final_0",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[3];h q[2]; cx q[2], q[0]; cx q[2], q[1];\n",
+    "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,
+    "coupling_map": "{0,2};{2,0};{1,0};{0,1}"
+  },
+  {
+    "description": "coupling_test_3qubit_cnots_at_0",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[3]; h q[0]; cx q[0], q[1]; s q[2]; cx q[1], q[2]; h q[2]; z q[0];\n",
+    "expected_minimal_gates": 5,
+    "expected_minimal_depth": 4,
+    "expected_minimal_gates_at_minimal_depth": 5,
+    "expected_minimal_two_qubit_gates": 2,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 5,
+    "coupling_map": "{0,2};{2,0};{1,0};{0,1}"
+  },
+  {
+    "description": "coupling_test_3qubit_cnots_at_1",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[3]; h q[0]; cx q[0], q[1]; s q[2]; cx q[1], q[2]; h q[2]; z q[0];\n",
+    "expected_minimal_gates": 5,
+    "expected_minimal_depth": 4,
+    "expected_minimal_gates_at_minimal_depth": 5,
+    "expected_minimal_two_qubit_gates": 2,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 5,
+    "coupling_map": "{1,2};{2,1};{1,0};{0,1}"
+  },
+  {
+    "description": "coupling_test_irred_3qubit_cnots_at_1",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[3]; h q[0]; cx q[0], q[1]; cx q[1], q[2]; x q[1]; h q[2]; cx q[2], q[1];\n",
+    "expected_minimal_gates": 6,
+    "expected_minimal_depth": 4,
+    "expected_minimal_gates_at_minimal_depth": 9,
+    "expected_minimal_two_qubit_gates": 2,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 8,
+    "coupling_map": "{1,2};{2,1};{1,0};{0,1}"
+  },
+  {
+    "description": "coupling_test_irred_3qubit_cnots_at_2",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[3]; h q[0]; cx q[0], q[1]; cx q[1], q[2]; x q[1]; h q[2]; cx q[2], q[1];\n",
+    "expected_minimal_gates": 6,
+    "expected_minimal_depth": 4,
+    "expected_minimal_gates_at_minimal_depth": 9,
+    "expected_minimal_two_qubit_gates": 2,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 8,
+    "coupling_map": "{0,2};{2,0};{2,1};{1,2}"
+  },
+  {
+    "description": "coupling_test_irred_3qubit_cnots_at_0",
+    "initial_circuit": "OPENQASM 2.0;include \"qelib1.inc\";qreg q[3]; h q[0]; cx q[0], q[1]; cx q[1], q[2]; x q[1]; h q[2]; cx q[2], q[1];\n",
+    "expected_minimal_gates": 6,
+    "expected_minimal_depth": 4,
+    "expected_minimal_gates_at_minimal_depth": 9,
+    "expected_minimal_two_qubit_gates": 2,
+    "expected_minimal_gates_at_minimal_two_qubit_gates": 8,
+    "coupling_map": "{0,2};{2,0};{0,1};{1,0}"
   }
 ]
diff --git a/test/cliffordsynthesis/test_synthesis.cpp b/test/cliffordsynthesis/test_synthesis.cpp
index 45b7c8c6c..5b7878c91 100644
--- a/test/cliffordsynthesis/test_synthesis.cpp
+++ b/test/cliffordsynthesis/test_synthesis.cpp
@@ -6,10 +6,14 @@
 #include "Definitions.hpp"
 #include "cliffordsynthesis/CliffordSynthesizer.hpp"
 #include "cliffordsynthesis/Results.hpp"
+#include "cliffordsynthesis/Tableau.hpp"
 #include "cliffordsynthesis/TargetMetric.hpp"
 #include "ir/QuantumComputation.hpp"
 #include "ir/operations/Control.hpp"
+#include "sc/utils.hpp"
 
+#include <algorithm>
+#include <cassert>
 #include <cstddef>
 #include <fstream>
 #include <gtest/gtest.h>
@@ -30,6 +34,7 @@ struct TestConfiguration {
   std::string initialTableau;
   std::string targetTableau;
   std::string initialCircuit;
+  std::string couplingMap;
 
   // expected output
   std::size_t expectedMinimalGates{};
@@ -51,6 +56,9 @@ inline void from_json(const nlohmann::json& j, TestConfiguration& test) {
   if (j.contains("initial_circuit")) {
     test.initialCircuit = j.at("initial_circuit").get<std::string>();
   }
+  if (j.contains("coupling_map")) {
+    test.couplingMap = j.at("coupling_map").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>();
@@ -72,6 +80,31 @@ std::vector<TestConfiguration> getTests(const std::string& path) {
 }
 } // namespace
 
+CouplingMap parseEdges(const std::string& edgeString) {
+  CouplingMap edges;
+  std::stringstream ss(edgeString);
+  std::string item;
+
+  while (getline(ss, item, ';')) {
+    item.erase(remove(item.begin(), item.end(), '{'), item.end());
+    item.erase(remove(item.begin(), item.end(), '}'), item.end());
+    const size_t pos = item.find(',');
+    std::string first;
+    std::string second;
+
+    first = item.substr(0, pos);
+    second = item.substr(pos + 1);
+
+    const int u = stoi(first);
+    const int v = stoi(second);
+
+    // Insert the edge into the set
+    edges.insert(Edge{u, v});
+    std::cout << "Edge " << u << "," << v << " inserted to cm\n";
+  }
+
+  return edges;
+}
 class SynthesisTest : public ::testing::TestWithParam<TestConfiguration> {
 protected:
   void SetUp() override {
@@ -88,8 +121,14 @@ class SynthesisTest : public ::testing::TestWithParam<TestConfiguration> {
       if (test.initialTableau.empty()) {
         initialTableau = Tableau(qc.getNqubits());
         initialTableauWithDestabilizer = Tableau(qc.getNqubits(), true);
-        synthesizer = CliffordSynthesizer(qc);
-        synthesizerWithDestabilizer = CliffordSynthesizer(qc, true);
+        if (test.couplingMap.empty()) {
+          synthesizer = CliffordSynthesizer(qc);
+          synthesizerWithDestabilizer = CliffordSynthesizer(qc, true);
+        } else {
+          synthesizer = CliffordSynthesizer(qc, parseEdges(test.couplingMap));
+          synthesizerWithDestabilizer =
+              CliffordSynthesizer(qc, parseEdges(test.couplingMap), true);
+        }
       } else {
         initialTableau = Tableau(test.initialTableau);
         std::cout << "Initial tableau:\n" << initialTableau;
@@ -117,9 +156,34 @@ class SynthesisTest : public ::testing::TestWithParam<TestConfiguration> {
   void TearDown() override {
     std::cout << "Results:\n" << results << "\n";
 
-    resultTableau = synthesizer.getResultTableau();
-    std::cout << "Resulting tableau:\n" << resultTableau;
-    EXPECT_EQ(resultTableau, targetTableau);
+    std::cout << "Mapping of Qubits:\n" << results.getMapping() << "\n";
+
+    resultTableau = Tableau(synthesizer.getResultTableau());
+
+    std::cout << "Result tableau:\n" << resultTableau;
+
+    std::cout << "Target tableau:\n" << targetTableau;
+
+    const std::vector<std::vector<bool>> p = results.getMappingVector();
+    Tableau targetPrime = targetTableau.applyMapping(p);
+    std::cout << "Target tableau with mapping:\n" << targetPrime;
+    if (!targetPrime.hasDestabilizers()) {
+      targetPrime.rref();
+      resultTableau.rref();
+      assert(targetPrime.equivalentUpToStabilizer(&resultTableau));
+      std::cout << "Target tableau with mapping and Gauss:\n" << targetPrime;
+      std::cout << "Result tableau with mapping and Gauss:\n" << resultTableau;
+    } else {
+      targetPrime =
+          targetPrime.reverseMappingOnRows(p, targetPrime.getQubitCount());
+      resultTableau =
+          resultTableau.reverseMappingOnRows(p, targetPrime.getQubitCount());
+      std::cout << "Result tableau with destab mapping reversed:\n"
+                << resultTableau;
+      std::cout << "Target tableau with destab mapping reversed:\n"
+                << targetPrime;
+    }
+    EXPECT_EQ(resultTableau, targetPrime);
 
     const auto& resultCircuit = synthesizer.getResultCircuit();
     std::cout << "Resulting Circuit:\n" << resultCircuit;
@@ -131,6 +195,11 @@ class SynthesisTest : public ::testing::TestWithParam<TestConfiguration> {
     for (const auto& gate : qc) {
       circuitTableau.applyGate(gate.get());
     }
+    std::cout << "Circuit Tableau :\n" << circuitTableau;
+    if (!circuitTableau.hasDestabilizers()) {
+      circuitTableau.rref();
+      std::cout << "Circuit Tableau with Gauss" << circuitTableau;
+    }
     EXPECT_EQ(resultTableau, circuitTableau);
   }
 
diff --git a/test/python/test_cliffordsynthesis.py b/test/python/test_cliffordsynthesis.py
index 7480ee3b0..ed45838a3 100644
--- a/test/python/test_cliffordsynthesis.py
+++ b/test/python/test_cliffordsynthesis.py
@@ -2,6 +2,7 @@
 
 from __future__ import annotations
 
+import itertools
 import json
 from dataclasses import dataclass
 from pathlib import Path
@@ -27,6 +28,31 @@ class Configuration:
     initial_tableau: str | None = None
     target_tableau: str | None = None
     initial_circuit: str | None = None
+    coupling_map: str | None = None
+
+
+def permute_qubits(circuit: QuantumCircuit, permutation: tuple[int, ...]) -> QuantumCircuit:
+    """Return a new circuit with qubits permuted according to the given permutation."""
+    permuted_circ = QuantumCircuit(circuit.num_qubits)
+    qubit_map = {qubit: i for i, qubit in enumerate(circuit.qubits)}
+
+    for d in circuit.data:
+        gate = d.operation
+        qubits = d.qubits
+        clbits = d.clbits
+        new_qubits = [circuit.qubits[permutation[qubit_map[q]]] for q in qubits]
+        permuted_circ.append(gate, new_qubits, clbits)
+
+    return permuted_circ
+
+
+def convert_coupling_map(cm: str | None = None) -> list[tuple[int, int]] | None:
+    """Convert a coupling map passed as a string to a CouplingMap."""
+    coupling_map = None
+    if cm is not None:
+        pairs = cm.split(";")
+        coupling_map = [(int(pair.strip("{}").split(",")[0]), int(pair.strip("{}").split(",")[1])) for pair in pairs]
+    return coupling_map
 
 
 def create_circuit_tests() -> list[Configuration]:
@@ -50,7 +76,10 @@ def create_tableau_tests() -> list[Configuration]:
 def test_optimize_clifford_gates(test_config: Configuration, use_maxsat: bool) -> None:
     """Test gate-optimal Clifford synthesis."""
     circ, results = qmap.optimize_clifford(
-        circuit=test_config.initial_circuit, use_maxsat=use_maxsat, target_metric="gates"
+        circuit=test_config.initial_circuit,
+        use_maxsat=use_maxsat,
+        target_metric="gates",
+        coupling_map=convert_coupling_map(test_config.coupling_map),
     )
 
     assert results.gates == test_config.expected_minimal_gates
@@ -62,7 +91,10 @@ def test_optimize_clifford_gates(test_config: Configuration, use_maxsat: bool) -
 def test_optimize_clifford_depth(test_config: Configuration, use_maxsat: bool) -> None:
     """Test depth-optimal Clifford synthesis."""
     circ, results = qmap.optimize_clifford(
-        circuit=test_config.initial_circuit, use_maxsat=use_maxsat, target_metric="depth"
+        circuit=test_config.initial_circuit,
+        use_maxsat=use_maxsat,
+        target_metric="depth",
+        coupling_map=convert_coupling_map(test_config.coupling_map),
     )
 
     assert results.depth == test_config.expected_minimal_depth
@@ -78,8 +110,8 @@ def test_optimize_clifford_gates_at_minimal_depth(test_config: Configuration, us
         use_maxsat=use_maxsat,
         target_metric="depth",
         minimize_gates_after_depth_optimization=True,
+        coupling_map=convert_coupling_map(test_config.coupling_map),
     )
-
     assert results.gates == test_config.expected_minimal_gates_at_minimal_depth
     print("\n", circ)
 
@@ -93,6 +125,7 @@ def test_optimize_clifford_two_qubit_gates(test_config: Configuration, use_maxsa
         use_maxsat=use_maxsat,
         target_metric="two_qubit_gates",
         try_higher_gate_limit_for_two_qubit_gate_optimization=True,
+        coupling_map=convert_coupling_map(test_config.coupling_map),
     )
 
     assert results.two_qubit_gates == test_config.expected_minimal_two_qubit_gates
@@ -109,6 +142,7 @@ def test_optimize_clifford_gates_at_minimal_two_qubit_gates(test_config: Configu
         target_metric="two_qubit_gates",
         try_higher_gate_limit_for_two_qubit_gate_optimization=True,
         minimize_gates_after_two_qubit_gate_optimization=True,
+        coupling_map=convert_coupling_map(test_config.coupling_map),
     )
 
     assert results.gates == test_config.expected_minimal_gates_at_minimal_two_qubit_gates
@@ -129,9 +163,17 @@ def test_heuristic(test_config: Configuration) -> None:
     circ_opt, _ = qmap.optimize_clifford(
         circuit=test_config.initial_circuit, heuristic=False, target_metric="depth", include_destabilizers=True
     )
-
     assert circ.depth() >= circ_opt.depth()
-    assert Clifford(circ) == Clifford(circ_opt)
+
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ_opt, perm)
+        if Clifford(permuted_circ) == Clifford(circ):
+            equivalent = True
+            break
+    assert equivalent
     print("\n", circ)
 
 
@@ -144,6 +186,7 @@ def test_synthesize_clifford_gates(test_config: Configuration, use_maxsat: bool)
         initial_tableau=test_config.initial_tableau,
         use_maxsat=use_maxsat,
         target_metric="gates",
+        coupling_map=convert_coupling_map(test_config.coupling_map),
     )
 
     assert results.gates == test_config.expected_minimal_gates
@@ -159,6 +202,7 @@ def test_synthesize_clifford_depth(test_config: Configuration, use_maxsat: bool)
         initial_tableau=test_config.initial_tableau,
         use_maxsat=use_maxsat,
         target_metric="depth",
+        coupling_map=convert_coupling_map(test_config.coupling_map),
     )
 
     assert results.depth == test_config.expected_minimal_depth
@@ -175,6 +219,7 @@ def test_synthesize_clifford_gates_at_minimal_depth(test_config: Configuration,
         use_maxsat=use_maxsat,
         target_metric="depth",
         minimize_gates_after_depth_optimization=True,
+        coupling_map=convert_coupling_map(test_config.coupling_map),
     )
 
     assert results.gates == test_config.expected_minimal_gates_at_minimal_depth
@@ -191,6 +236,7 @@ def test_synthesize_clifford_two_qubit_gates(test_config: Configuration, use_max
         use_maxsat=use_maxsat,
         target_metric="two_qubit_gates",
         try_higher_gate_limit_for_two_qubit_gate_optimization=True,
+        coupling_map=convert_coupling_map(test_config.coupling_map),
     )
 
     assert results.two_qubit_gates == test_config.expected_minimal_two_qubit_gates
@@ -208,6 +254,7 @@ def test_synthesize_clifford_gates_at_minimal_two_qubit_gates(test_config: Confi
         target_metric="two_qubit_gates",
         try_higher_gate_limit_for_two_qubit_gate_optimization=True,
         minimize_gates_after_two_qubit_gate_optimization=True,
+        coupling_map=convert_coupling_map(test_config.coupling_map),
     )
 
     assert results.gates == test_config.expected_minimal_gates_at_minimal_two_qubit_gates
@@ -231,54 +278,184 @@ 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, _ = qmap.optimize_clifford(circuit=qc)
-    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ, perm)
+        if qcec.verify(permuted_circ, bell_circuit).considered_equivalent():
+            equivalent = True
+            break
+    assert equivalent
 
 
 def test_optimize_from_qasm_file(bell_circuit: QuantumCircuit) -> None:
     """Test that we can optimize from a QASM file."""
     qasm2.dump(bell_circuit, Path("bell.qasm"))
     circ, _ = qmap.optimize_clifford(circuit="bell.qasm")
-    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ, perm)
+        if qcec.verify(permuted_circ, bell_circuit).considered_equivalent():
+            equivalent = True
+            break
+    assert equivalent
 
 
 def test_optimize_qiskit_circuit(bell_circuit: QuantumCircuit) -> None:
     """Test that we can optimize a Qiskit QuantumCircuit."""
     circ, _ = qmap.optimize_clifford(circuit=bell_circuit)
-    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ, perm)
+        if qcec.verify(permuted_circ, bell_circuit).considered_equivalent():
+            equivalent = True
+            break
+    assert equivalent
 
 
 def test_optimize_with_initial_tableau(bell_circuit: QuantumCircuit) -> None:
     """Test that we can optimize a circuit with an initial tableau."""
     circ, _ = qmap.optimize_clifford(circuit=bell_circuit, initial_tableau=qmap.Tableau(bell_circuit.num_qubits))
-    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ, perm)
+        if qcec.verify(permuted_circ, bell_circuit).considered_equivalent():
+            equivalent = True
+            break
+    assert equivalent
+
+
+def test_optimize_with_initial_tableau_with_mapping(bell_circuit: QuantumCircuit) -> None:
+    """Test that we can optimize a circuit with an initial tableau."""
+    coupling_map = [(0, 1), (1, 0)]
+    circ, _ = qmap.optimize_clifford(
+        circuit=bell_circuit, initial_tableau=qmap.Tableau(bell_circuit.num_qubits), coupling_map=coupling_map
+    )
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ, perm)
+        if qcec.verify(permuted_circ, bell_circuit).considered_equivalent():
+            equivalent = True
+            break
+    assert 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, _ = qmap.synthesize_clifford(target_tableau=tableau)
-    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ, perm)
+        if qcec.verify(permuted_circ, bell_circuit).considered_equivalent():
+            equivalent = True
+            break
+    assert 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, _ = qmap.synthesize_clifford(target_tableau=cliff)
-    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ, perm)
+        if qcec.verify(permuted_circ, bell_circuit).considered_equivalent():
+            equivalent = True
+            break
+    assert 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, _ = qmap.synthesize_clifford(target_tableau=pauli_list)
-    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ, perm)
+        if qcec.verify(permuted_circ, bell_circuit).considered_equivalent():
+            equivalent = True
+            break
+    assert equivalent
 
 
 def test_synthesize_from_string(bell_circuit: QuantumCircuit) -> None:
     """Test that we can synthesize a circuit from a String."""
     pauli_str = "[XX,ZZ]"
     circ, _ = qmap.synthesize_clifford(target_tableau=pauli_str)
-    assert qcec.verify(circ, bell_circuit).considered_equivalent()
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ, perm)
+        if qcec.verify(permuted_circ, bell_circuit).considered_equivalent():
+            equivalent = True
+            break
+    assert equivalent
+
+
+def test_synthesize_with_coupling_from_tableau(bell_circuit: QuantumCircuit) -> None:
+    """Test that we can synthesize a circuit from an MQT Tableau."""
+    tableau = qmap.Tableau("['XX', 'ZZ']")
+    coupling_map = [(0, 1), (1, 0)]
+    circ, _ = qmap.synthesize_clifford(target_tableau=tableau, coupling_map=coupling_map)
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ, perm)
+        if qcec.verify(permuted_circ, bell_circuit).considered_equivalent():
+            equivalent = True
+            break
+    assert equivalent
+
+
+def test_synthesize_with_coupling_with_initial_tableau_from_tableau(bell_circuit: QuantumCircuit) -> None:
+    """Test that we can synthesize a circuit from an MQT Tableau."""
+    tableau = qmap.Tableau("['XX', 'ZZ']")
+    init_tableau = qmap.Tableau("['ZI','IZ']")
+    coupling_map = [(0, 1), (1, 0)]
+    circ, _ = qmap.synthesize_clifford(target_tableau=tableau, initial_tableau=init_tableau, coupling_map=coupling_map)
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ, perm)
+        if qcec.verify(permuted_circ, bell_circuit).considered_equivalent():
+            equivalent = True
+            break
+    assert equivalent
+
+
+def test_synthesize_with_coupling_with_initial_tableau_from_qc(bell_circuit: QuantumCircuit) -> None:
+    """Test that we can synthesize a circuit from an MQT Tableau."""
+    init_tableau = qmap.Tableau("['ZI','IZ']")
+    coupling_map = [(0, 1), (1, 0)]
+    circ, _ = qmap.optimize_clifford(circuit=bell_circuit, initial_tableau=init_tableau, coupling_map=coupling_map)
+    num_qubits = circ.num_qubits
+    qubit_permutations = list(itertools.permutations(range(num_qubits)))
+    equivalent = False
+    for perm in qubit_permutations:
+        permuted_circ = permute_qubits(circ, perm)
+        if qcec.verify(permuted_circ, bell_circuit).considered_equivalent():
+            equivalent = True
+            break
+    assert equivalent
 
 
 def test_invalid_kwarg_to_synthesis() -> None: