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

Issue:
Custom encodings not working
There seems to be a bug in the custom `commander` and `bimander` encodings. The following MWE (added as an additional test case to the `test_exact.cpp` file) produces very unexpected results:

```c++
TEST_F(ExactTest, MWE) {
    using namespace dd::literals;

    auto circ = qc::QuantumComputation(3U);
    circ.x(2, 1_pc);
    circ.x(1, 0_pc);

    auto arch = Architecture("../../extern/architectures/ibmq_casablanca.arch");

    auto mapper = ExactMapper(circ, arch);
    auto settings = Configuration();
    settings.useSubsets = false;
    settings.encoding = Encoding::Commander; // or Encoding::Bimander
    settings.commanderGrouping = CommanderGrouping::Halves; // or CommanderGrouping::Fixed2, CommanderGrouping::Fixed3, CommanderGrouping::Logarithm
    mapper.map(settings);
    mapper.printResult(std::cout);
}
```

The results (running under `macOS 12.3.1` using `z3-4.8.17`) can be summarized as follows:

Encoding | Grouping | Result
--- | --- | ---
None | - | Optimal solution (0 SWAPs) within 2.5s
Commander | Halves | Suboptimal solution (1 SWAP) within 2.5s
\- | Fixed2 | z3 returns `UNSAT` within a fraction of a second
\- | Fixed3 | Optimal solution (0 SWAPs) within 3.2s
\- | Logarithm | Takes forever (>5min) then segfaults
Bimander | Halves | Suboptimal solution (2 SWAPs) within 2.3s
\- | Fixed2 | z3 returns `UNSAT` within a fraction of a second
\- | Fixed3 | Suboptimal solution (2 SWAPs) within 2.0s
\- | Logarithm | Takes forever (>5min) then segfaults


Discussion / hints:
This is fixed by #59.
Unfortunately, the underlying issue is still not fixed. Mapping the following circuit produces `UNSAT` for all encoding variants:
```c++
    qc = qc::QuantumComputation(5U);
    qc.x(1, 0_pc);
    qc.x(2, 0_pc);
    qc.x(3, 0_pc);
    qc.x(4, 0_pc);

    arch = Architecture("../../extern/architectures/ibmq_casablanca.arch");

    mapper = std::make_unique<ExactMapper>(qc, arch);

    settings.verbose = true;
    settings.method  = Method::Exact;
    settings.useSubsets = false;
```
I identified the problem and a fix is on the way.

Fix patch:
diff --git a/README.md b/README.md
index e223ed103..b1846acf4 100644
--- a/README.md
+++ b/README.md
@@ -92,6 +92,7 @@ Architectures that are available per default (either as strings or under `qmap.A
 - `IBMQ_Yorktown` (5 qubit, undirected bow tie layout)
 - `IBMQ_London` (5 qubit, undirected T-shape layout)
 - `IBMQ_Bogota` (5 qubit, undirected linear chain layout)
+- `IBMQ_Casablanca` (7 qubit, undirected H-shape layout)
 - `IBMQ_Tokyo` (20 qubit, undirected brick-like layout)
 
 Whether the heuristic (*default*) or the exact mapper is used can be controlled by passing `method="heuristic"` or `method="exact"` to the `compile` function.
diff --git a/include/configuration/AvailableArchitecture.hpp b/include/configuration/AvailableArchitecture.hpp
index 4fd92c989..8f80457dd 100644
--- a/include/configuration/AvailableArchitecture.hpp
+++ b/include/configuration/AvailableArchitecture.hpp
@@ -15,6 +15,7 @@ enum class AvailableArchitecture {
     IBMQ_Yorktown,
     IBMQ_London,
     IBMQ_Bogota,
+    IBMQ_Casablanca,
     IBMQ_Tokyo
 };
 
@@ -30,6 +31,8 @@ enum class AvailableArchitecture {
             return "IBMQ_London";
         case AvailableArchitecture::IBMQ_Bogota:
             return "IBMQ_Bogota";
+        case AvailableArchitecture::IBMQ_Casablanca:
+            return "IBMQ_Casablanca";
         case AvailableArchitecture::IBMQ_Tokyo:
             return "IBMQ_Tokyo";
     }
@@ -47,7 +50,9 @@ enum class AvailableArchitecture {
         return AvailableArchitecture::IBMQ_London;
     } else if (architecture == "IBMQ_Bogota" || architecture == "4") {
         return AvailableArchitecture::IBMQ_Bogota;
-    } else if (architecture == "IBMQ_Tokyo" || architecture == "5") {
+    } else if (architecture == "IBMQ_Casablanca" || architecture == "5") {
+        return AvailableArchitecture::IBMQ_Casablanca;
+    } else if (architecture == "IBMQ_Tokyo" || architecture == "6") {
         return AvailableArchitecture::IBMQ_Tokyo;
     } else {
         throw std::invalid_argument("Invalid architecture value: " + architecture);
@@ -61,6 +66,7 @@ enum class AvailableArchitecture {
             {AvailableArchitecture::IBMQ_Yorktown, "5\n0 1\n1 0\n0 2\n2 0\n1 2\n2 1\n2 3\n3 2\n3 4\n4 3\n2 4\n4 2"},
             {AvailableArchitecture::IBMQ_London, "5\n0 1\n1 0\n1 2\n2 1\n1 3\n3 1\n3 4\n4 3"},
             {AvailableArchitecture::IBMQ_Bogota, "5\n0 1\n1 0\n1 2\n2 1\n2 3\n3 2\n3 4\n4 3"},
+            {AvailableArchitecture::IBMQ_Casablanca, "7\n0 1\n1 0\n1 2\n2 1\n1 3\n3 1\n3 5\n5 3\n5 4\n4 5\n5 6\n6 5"},
             {AvailableArchitecture::IBMQ_Tokyo, "20\n0 1\n1 0\n1 2\n2 1\n2 3\n3 2\n3 4\n4 3\n5 6\n6 5\n6 7\n7 6\n7 8\n8 7\n8 9\n9 8\n10 11\n11 10\n11 12\n12 11\n12 13\n13 12\n13 14\n14 13\n15 16\n16 15\n16 17\n17 16\n17 18\n18 17\n18 19\n19 18\n0 5\n5 0\n5 10\n10 5\n10 15\n15 10\n1 6\n6 1\n6 11\n11 6\n11 16\n16 11\n2 7\n7 2\n7 12\n12 7\n12 17\n17 12\n3 8\n8 3\n8 13\n13 8\n13 18\n18 13\n4 9\n9 4\n9 14\n14 9\n14 19\n19 14\n5 11\n11 5\n11 17\n17 11\n1 7\n7 1\n7 13\n13 7\n13 9\n9 13\n3 9\n9 3\n2 6\n6 2\n6 10\n10 6\n4 8\n8 4\n8 12\n12 8\n12 16\n16 12\n14 18\n18 14"}};
     return architectureMap.at(architecture);
 }
diff --git a/src/Encodings.cpp b/src/Encodings.cpp
index d740d4575..dd143be06 100644
--- a/src/Encodings.cpp
+++ b/src/Encodings.cpp
@@ -206,5 +206,5 @@ expr varAlloc(expr_vector& auxvars, z3::context& c) {
     std::stringstream out;
     out << "c_" << nextVar++;
     auxvars.push_back(c.bool_const(out.str().c_str()));
-    return auxvars[static_cast<int>(auxvars.size() - 1)];
+    return auxvars.back();
 }
diff --git a/src/exact/ExactMapper.cpp b/src/exact/ExactMapper.cpp
index 230e10c72..7f3db5b1b 100644
--- a/src/exact/ExactMapper.cpp
+++ b/src/exact/ExactMapper.cpp
@@ -470,13 +470,13 @@ void ExactMapper::coreMappingRoutine(const std::set<unsigned short>& qubitChoice
                     varIDs.push_back(x[k][i][j]);
                 }
                 if (config.commanderGrouping == CommanderGrouping::Fixed2) {
-                    opt.add(AtMostOneCMDR(varIDs, groupVars(varIDs, 2), static_cast<int>(auxvars.size() - 1), auxvars, c));
+                    opt.add(AtMostOneCMDR(varIDs, groupVars(varIDs, 2), -1, auxvars, c));
                 } else if (config.commanderGrouping == CommanderGrouping::Fixed3) {
-                    opt.add(AtMostOneCMDR(varIDs, groupVars(varIDs, 3), static_cast<int>(auxvars.size() - 1), auxvars, c));
+                    opt.add(AtMostOneCMDR(varIDs, groupVars(varIDs, 3), -1, auxvars, c));
                 } else if (config.commanderGrouping == CommanderGrouping::Logarithm) {
-                    opt.add(AtMostOneCMDR(varIDs, groupVars(varIDs, static_cast<std::size_t>(std::log(varIDs.size()))), static_cast<int>(auxvars.size() - 1), auxvars, c));
+                    opt.add(AtMostOneCMDR(varIDs, groupVars(varIDs, static_cast<std::size_t>(std::log(varIDs.size()))), -1, auxvars, c));
                 } else if (config.commanderGrouping == CommanderGrouping::Halves) {
-                    opt.add(AtMostOneCMDR(varIDs, groupVars(varIDs, varIDs.size() / 2), static_cast<int>(auxvars.size() - 1), auxvars, c));
+                    opt.add(AtMostOneCMDR(varIDs, groupVars(varIDs, varIDs.size() / 2), -1, auxvars, c));
                 }
             }
 
@@ -487,13 +487,13 @@ void ExactMapper::coreMappingRoutine(const std::set<unsigned short>& qubitChoice
                 }
 
                 if (config.commanderGrouping == CommanderGrouping::Fixed2) {
-                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, 2), static_cast<int>(auxvars.size() - 1), auxvars, c));
+                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, 2), -1, auxvars, c));
                 } else if (config.commanderGrouping == CommanderGrouping::Fixed3) {
-                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, 3), static_cast<int>(auxvars.size() - 1), auxvars, c));
+                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, 3), -1, auxvars, c));
                 } else if (config.commanderGrouping == CommanderGrouping::Logarithm) {
-                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, static_cast<std::size_t>(std::log(varIDs.size()))), static_cast<int>(auxvars.size() - 1), auxvars, c));
+                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, static_cast<std::size_t>(std::log(varIDs.size()))), -1, auxvars, c));
                 } else if (config.commanderGrouping == CommanderGrouping::Halves) {
-                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, varIDs.size() / 2), static_cast<int>(auxvars.size() - 1), auxvars, c));
+                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, varIDs.size() / 2), -1, auxvars, c));
                 }
             }
         }
@@ -516,13 +516,13 @@ void ExactMapper::coreMappingRoutine(const std::set<unsigned short>& qubitChoice
                 }
 
                 if (config.commanderGrouping == CommanderGrouping::Fixed2) {
-                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, 2), static_cast<int>(auxvars.size() - 1), auxvars, c));
+                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, 2), -1, auxvars, c));
                 } else if (config.commanderGrouping == CommanderGrouping::Fixed3) {
-                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, 3), static_cast<int>(auxvars.size() - 1), auxvars, c));
+                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, 3), -1, auxvars, c));
                 } else if (config.commanderGrouping == CommanderGrouping::Logarithm) {
-                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, static_cast<std::size_t>(std::log(varIDs.size()))), static_cast<int>(auxvars.size() - 1), auxvars, c));
+                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, static_cast<std::size_t>(std::log(varIDs.size()))), -1, auxvars, c));
                 } else if (config.commanderGrouping == CommanderGrouping::Halves) {
-                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, varIDs.size() / 2), static_cast<int>(auxvars.size() - 1), auxvars, c));
+                    opt.add(ExactlyOneCMDR(varIDs, groupVars(varIDs, varIDs.size() / 2), -1, auxvars, c));
                 }
             }
         }


Test patch:
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index e0f8528f7..6ceb138a2 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -43,5 +43,6 @@ package_add_test(${PROJECT_NAME}_heuristic_test heuristic
 
 if (TARGET ${PROJECT_NAME}_exact_lib)
 	package_add_test(${PROJECT_NAME}_exact_test exact
-	                 ${CMAKE_CURRENT_SOURCE_DIR}/test_exact.cpp)
+	                 ${CMAKE_CURRENT_SOURCE_DIR}/test_exact.cpp
+	                 ${CMAKE_CURRENT_SOURCE_DIR}/test_encodings.cpp)
 endif ()
diff --git a/test/test_encodings.cpp b/test/test_encodings.cpp
new file mode 100644
index 000000000..65dda52f2
--- /dev/null
+++ b/test/test_encodings.cpp
@@ -0,0 +1,77 @@
+#include "exact/ExactMapper.hpp"
+
+#include "gtest/gtest.h"
+
+class TestEncodings: public testing::TestWithParam<std::pair<Encoding, CommanderGrouping>> {
+protected:
+    std::string test_example_dir      = "./examples/";
+    std::string test_architecture_dir = "./architectures/";
+    std::string test_calibration_dir  = "./calibration/";
+
+    qc::QuantumComputation       qc{};
+    Configuration                settings{};
+    Architecture                 arch{};
+    std::unique_ptr<ExactMapper> mapper{};
+
+    void SetUp() override {
+        settings.verbose    = true;
+        settings.method     = Method::Exact;
+        settings.useSubsets = false;
+    }
+};
+
+INSTANTIATE_TEST_SUITE_P(Encodings, TestEncodings,
+                         testing::Values(
+                                 std::pair{Encoding::Naive, CommanderGrouping::Halves},
+                                 std::pair{Encoding::Commander, CommanderGrouping::Halves},
+                                 std::pair{Encoding::Commander, CommanderGrouping::Fixed2},
+                                 std::pair{Encoding::Commander, CommanderGrouping::Fixed3},
+                                 std::pair{Encoding::Bimander, CommanderGrouping::Halves},
+                                 std::pair{Encoding::Bimander, CommanderGrouping::Fixed2},
+                                 std::pair{Encoding::Bimander, CommanderGrouping::Fixed3}));
+
+TEST_P(TestEncodings, ThreeToSevenQubits) {
+    using namespace dd::literals;
+
+    qc = qc::QuantumComputation(3U);
+    qc.x(2, 1_pc);
+    qc.x(1, 0_pc);
+
+    arch.loadCouplingMap(AvailableArchitecture::IBMQ_Casablanca);
+
+    mapper = std::make_unique<ExactMapper>(qc, arch);
+
+    const auto& [encoding, grouping] = GetParam();
+    settings.encoding                = encoding;
+    settings.commanderGrouping       = grouping;
+
+    mapper->map(settings);
+    mapper->printResult(std::cout);
+
+    ASSERT_FALSE(mapper->getResults().timeout);
+    EXPECT_EQ(mapper->getResults().output.swaps, 0U);
+}
+
+TEST_P(TestEncodings, FiveToSevenQubits) {
+    using namespace dd::literals;
+
+    qc = qc::QuantumComputation(5U);
+    qc.x(1, 0_pc);
+    qc.x(2, 0_pc);
+    qc.x(3, 0_pc);
+    qc.x(4, 0_pc);
+
+    arch.loadCouplingMap(AvailableArchitecture::IBMQ_Casablanca);
+
+    mapper = std::make_unique<ExactMapper>(qc, arch);
+
+    const auto& [encoding, grouping] = GetParam();
+    settings.encoding                = encoding;
+    settings.commanderGrouping       = grouping;
+
+    mapper->map(settings);
+    mapper->printResult(std::cout);
+
+    ASSERT_FALSE(mapper->getResults().timeout);
+    EXPECT_EQ(mapper->getResults().output.swaps, 1U);
+}