cda-tum · avelsh · Jun 23, 2023 · Jun 23, 2023 · Jun 23, 2023 · Jul 8, 2023
diff --git a/extern/LogicBlocks b/extern/LogicBlocks
diff --git a/extern/mqt-core b/extern/mqt-core
diff --git a/include/cliffordsynthesis/CliffordSynthesizer.hpp b/include/cliffordsynthesis/CliffordSynthesizer.hpp
@@ -81,6 +81,10 @@ class CliffordSynthesizer {
     return metric == TargetMetric::Depth;
   }
 
+  static bool requiresTwoQubitEncoding(const TargetMetric metric) {
+    return metric == TargetMetric::TwoQubitDepth;
+  }
+
   void determineInitialTimestepLimit(EncoderConfig& config);
   std::pair<std::size_t, std::size_t> determineUpperBound(EncoderConfig config);
   void                                runMaxSAT(const EncoderConfig& config);
@@ -92,6 +96,8 @@ class CliffordSynthesizer {
                             std::size_t upper);
   void depthOptimalSynthesis(EncoderConfig config, std::size_t lower,
                              std::size_t upper);
+  void twoQubitDepthOptimalSynthesis(EncoderConfig config, std::size_t lower,
+                                     std::size_t upper);
   void depthHeuristicSynthesis();
   void twoQubitGateOptimalSynthesis(EncoderConfig config, std::size_t lower,
                                     std::size_t upper);

diff --git a/include/cliffordsynthesis/Configuration.hpp b/include/cliffordsynthesis/Configuration.hpp
@@ -38,6 +38,9 @@ struct Configuration {
   /// Settings for depth-optimal synthesis
   bool minimizeGatesAfterDepthOptimization = false;
 
+  /// Settings for TwoQubitDepth-optimal synthesis
+  bool useTwoQubitEncoding = false;
+
   /// Settings for two-qubit gate-optimal synthesis
   bool   tryHigherGateLimitForTwoQubitGateOptimization = false;
   double gateLimitFactor                               = 1.1;
@@ -63,9 +66,10 @@ struct Configuration {
     j["gate_limit_factor"] = gateLimitFactor;
     j["minimize_gates_after_two_qubit_gate_optimization"] =
         minimizeGatesAfterTwoQubitGateOptimization;
-    j["heuristic"]           = heuristic;
-    j["split_size"]          = splitSize;
-    j["n_threads_heuristic"] = nThreadsHeuristic;
+    j["use_two_qubit_encoding"] = useTwoQubitEncoding;
+    j["heuristic"]              = heuristic;
+    j["split_size"]             = splitSize;
+    j["n_threads_heuristic"]    = nThreadsHeuristic;
     if (!solverParameters.empty()) {
       nlohmann::json solverParametersJson;
       for (const auto& entry : solverParameters) {
@@ -77,6 +81,7 @@ struct Configuration {
       }
       j["solver_parameters"] = solverParametersJson;
     }
+
     return j;
   }
 

diff --git a/include/cliffordsynthesis/Results.hpp b/include/cliffordsynthesis/Results.hpp
@@ -25,6 +25,7 @@ class Results {
     setResultCircuit(qc);
     setResultTableau(tableau);
     setDepth(qc.getDepth());
+    setTwoQubitDepth(qc.getTwoQubitDepth());
     setSingleQubitGates(qc.getNsingleQubitOps());
     setTwoQubitGates(qc.getNindividualOps() - singleQubitGates);
     setSolverResult(logicbase::Result::SAT);
@@ -39,8 +40,9 @@ class Results {
   [[nodiscard]] std::size_t getSingleQubitGates() const {
     return singleQubitGates;
   }
-  [[nodiscard]] std::size_t       getDepth() const { return depth; }
-  [[nodiscard]] double            getRuntime() const { return runtime; }
+  [[nodiscard]] std::size_t getDepth() const { return depth; }
+  [[nodiscard]] std::size_t getTwoQubitDepth() const { return twoQubitDepth; }
+  [[nodiscard]] double      getRuntime() const { return runtime; }
   [[nodiscard]] logicbase::Result getSolverResult() const {
     return solverResult;
   }
@@ -52,6 +54,7 @@ class Results {
   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 setTwoQubitDepth(const std::size_t d) { twoQubitDepth = 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; }
@@ -80,6 +83,7 @@ class Results {
     resultJSON["single_qubit_gates"] = singleQubitGates;
     resultJSON["two_qubit_gates"]    = twoQubitGates;
     resultJSON["depth"]              = depth;
+    resultJSON["twoQubitDepth"]      = twoQubitDepth;
     resultJSON["runtime"]            = runtime;
     resultJSON["solver_calls"]       = solverCalls;
 
@@ -96,8 +100,10 @@ class Results {
   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::size_t       twoQubitDepth    = std::numeric_limits<std::size_t>::max();
+
+  double      runtime     = 0.0;
+  std::size_t solverCalls = 0U;
 
   std::string resultTableau{};
   std::string resultCircuit{};

diff --git a/include/cliffordsynthesis/TargetMetric.hpp b/include/cliffordsynthesis/TargetMetric.hpp
@@ -9,7 +9,7 @@
 #include <string>
 
 namespace cs {
-enum class TargetMetric { Gates, TwoQubitGates, Depth };
+enum class TargetMetric { Gates, TwoQubitGates, Depth, TwoQubitDepth };
 
 [[maybe_unused]] static inline std::string toString(const TargetMetric target) {
   switch (target) {
@@ -19,6 +19,8 @@ enum class TargetMetric { Gates, TwoQubitGates, Depth };
     return "two_qubit_gates";
   case TargetMetric::Depth:
     return "depth";
+  case TargetMetric::TwoQubitDepth:
+    return "two_qubit_depth";
   }
   return "Error";
 }
@@ -34,6 +36,9 @@ targetMetricFromString(const std::string& target) {
   if (target == "depth") {
     return TargetMetric::Depth;
   }
+  if (target == "two_qubit_depth") {
+    return TargetMetric::TwoQubitDepth;
+  }
   return TargetMetric::Gates;
 }
 } // namespace cs
diff --git a/include/cliffordsynthesis/encoding/GateEncoder.hpp b/include/cliffordsynthesis/encoding/GateEncoder.hpp
@@ -40,8 +40,8 @@ class GateEncoder {
   };
 
   // variable creation
-  void createSingleQubitGateVariables();
-  void createTwoQubitGateVariables();
+  virtual void createSingleQubitGateVariables();
+  virtual void createTwoQubitGateVariables();
 
   // encode the relation between the tableaus and the gates
   virtual void encodeGates() {
@@ -52,13 +52,17 @@ class GateEncoder {
   virtual void encodeSymmetryBreakingConstraints();
 
   // extracting the circuit
-  void extractCircuitFromModel(Results& res, logicbase::Model& model);
+  virtual 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};
+  // TODO: set back
+  static constexpr std::array<qc::OpType, 4> SINGLE_QUBIT_GATES = {
+      qc::OpType::None, qc::OpType::H, qc::OpType::S, qc::OpType::SX};
+
+  // 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) {
@@ -130,9 +134,9 @@ class GateEncoder {
   virtual void assertSingleQubitGateConstraints(std::size_t pos) = 0;
   virtual void assertTwoQubitGateConstraints(std::size_t pos)    = 0;
   [[nodiscard]] static std::vector<TransformationFamily>
-       collectGateTransformations(std::size_t pos, std::size_t qubit,
-                                  const GateToTransformation& gateToTransformation);
-  void assertGatesImplyTransform(
+               collectGateTransformations(std::size_t pos, std::size_t qubit,
+                                          const GateToTransformation& gateToTransformation);
+  virtual void assertGatesImplyTransform(
       std::size_t pos, std::size_t qubit,
       const std::vector<TransformationFamily>& transformations);
   virtual void assertZConstraints(std::size_t pos, std::size_t qubit);
@@ -142,10 +146,10 @@ class GateEncoder {
   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);
+  virtual 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);

diff --git a/include/cliffordsynthesis/encoding/SATEncoder.hpp b/include/cliffordsynthesis/encoding/SATEncoder.hpp
@@ -50,6 +50,12 @@ class SATEncoder {
     // whether to use symmetry breaking
     bool useSymmetryBreaking = false;
 
+    // whether to use two qubit encoding
+    bool useTwoQubitEncoding = 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;
 

diff --git a/include/cliffordsynthesis/encoding/TwoQubitEncoder.hpp b/include/cliffordsynthesis/encoding/TwoQubitEncoder.hpp
@@ -0,0 +1,77 @@
+//
+// Created by Velsh Aleksei on 16.06.23.
+//
+
+#pragma once
+
+#include "cliffordsynthesis/encoding/GateEncoder.hpp"
+
+#include <cstddef>
+#include <optional>
+
+namespace cs::encoding {
+
+class TwoQubitEncoder : public GateEncoder {
+public:
+  using GateEncoder::GateEncoder;
+
+protected:
+  // define variables
+  logicbase::LogicTerm   rChanges{};
+  logicbase::LogicMatrix xorHelpers{};
+  logicbase::LogicMatrix gP{};
+
+  static constexpr std::array<qc::OpType, 4> PAULI_GATES = {
+      qc::OpType::None, qc::OpType::X, qc::OpType::Y, qc::OpType::Z};
+
+  [[nodiscard]] constexpr std::size_t
+  paulieGateToIndex(const qc::OpType type) {
+    for (std::size_t i = 0; i < PAULI_GATES.size(); ++i) {
+      if (PAULI_GATES.at(i) == type) {
+        return i;
+      }
+    }
+    return 0;
+  }
+
+  // variable creation
+  virtual void createSingleQubitGateVariables() override;
+  virtual void createTwoQubitGateVariables() override;
+  void         createPauliGateVariables();
+
+  // create constrains
+  [[nodiscard]] logicbase::LogicTerm
+  createTwoQubitGateConstraint(std::size_t pos, std::size_t ctrl,
+                               std::size_t trgt) override;
+
+  // assert constrains
+  void assertConsistency() const override;
+  void assertGateConstraints() override;
+  void assertRConstraints(std::size_t pos, std::size_t qubit) override;
+  void assertSingleQubitGateConstraints(std::size_t pos) override;
+  void assertPauliGateConstraints(std::size_t pos);
+  void assertTwoQubitGateConstraints(std::size_t pos) 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;
+
+  // collect TQG variables
+  void collectPauliGateVariables(std::size_t             qubit,
+                                 logicbase::LogicVector& variables) const;
+
+  // extracting
+  void extractCircuitFromModel(Results& res, logicbase::Model& model) override;
+  void extractPauliGatesFromModel(logicbase::Model&       model,
+                                  qc::QuantumComputation& qc,
+                                  std::size_t&            nSingleQubitGates);
+
+  // helpers
+  void         splitXorR(const logicbase::LogicTerm& changes, std::size_t pos);
+  virtual void assertGatesImplyTransform(
+      std::size_t pos, std::size_t qubit,
+      const std::vector<TransformationFamily>& transformations) override;
+  virtual void encodeSymmetryBreakingConstraints() override;
+};
+
+} // namespace cs::encoding
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -60,6 +60,7 @@ macro(ADD_SYNTHESIS_LIBRARY libname srcfile)
     ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/Configuration.hpp
     ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/encoding/GateEncoder.hpp
     ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/encoding/MultiGateEncoder.hpp
+    ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/encoding/TwoQubitEncoder.hpp
     ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/encoding/ObjectiveEncoder.hpp
     ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/encoding/SATEncoder.hpp
     ${PROJECT_SOURCE_DIR}/include/cliffordsynthesis/encoding/SingleGateEncoder.hpp
@@ -70,6 +71,7 @@ macro(ADD_SYNTHESIS_LIBRARY libname srcfile)
     ${PROJECT_SOURCE_DIR}/include/utils.hpp
     cliffordsynthesis/encoding/GateEncoder.cpp
     cliffordsynthesis/encoding/MultiGateEncoder.cpp
+    cliffordsynthesis/encoding/TwoQubitEncoder.cpp
     cliffordsynthesis/encoding/ObjectiveEncoder.cpp
     cliffordsynthesis/encoding/SATEncoder.cpp
     cliffordsynthesis/encoding/SingleGateEncoder.cpp