Feature/TwoQubitEncoding

include/cliffordsynthesis/CliffordSynthesizer.hpp

@@ -81,6 +81,10 @@ class CliffordSynthesizer {
     return metric == TargetMetric::Depth;
   }
 
+  static bool requiresTwoQubitEncoding(const TargetMetric metric) {
+    return metric == TargetMetric::TQDepth;
+  }
+
   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);

include/cliffordsynthesis/Configuration.hpp

@@ -38,6 +38,9 @@ struct Configuration {
   /// Settings for depth-optimal synthesis
   bool minimizeGatesAfterDepthOptimization = false;
 
+  /// Settings for STDepth-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;
   }
 

include/cliffordsynthesis/Results.hpp

@@ -40,6 +40,7 @@ class Results {
     return singleQubitGates;
   }
   [[nodiscard]] std::size_t       getDepth() const { return depth; }
+  [[nodiscard]] std::size_t       getTQDepth() const { return tQDepth; }
   [[nodiscard]] double            getRuntime() const { return runtime; }
   [[nodiscard]] logicbase::Result getSolverResult() const {
     return solverResult;
@@ -52,6 +53,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 setTQDepth(const std::size_t d) { tQDepth = 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 +82,7 @@ class Results {
     resultJSON["single_qubit_gates"] = singleQubitGates;
     resultJSON["two_qubit_gates"]    = twoQubitGates;
     resultJSON["depth"]              = depth;
+    resultJSON["tQDepth"]            = tQDepth;
     resultJSON["runtime"]            = runtime;
     resultJSON["solver_calls"]       = solverCalls;
 
@@ -96,8 +99,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       tQDepth          = std::numeric_limits<std::size_t>::max();
+
+  double      runtime     = 0.0;
+  std::size_t solverCalls = 0U;
 
   std::string resultTableau{};
   std::string resultCircuit{};

include/cliffordsynthesis/TargetMetric.hpp

@@ -9,7 +9,7 @@
 #include <string>
 
 namespace cs {
-enum class TargetMetric { Gates, TwoQubitGates, Depth };
+enum class TargetMetric { Gates, TwoQubitGates, Depth, TQDepth };
 
 [[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::TQDepth:
+    return "tQDepth";
   }
   return "Error";
 }
@@ -34,6 +36,9 @@ targetMetricFromString(const std::string& target) {
   if (target == "depth") {
     return TargetMetric::Depth;
   }
+  if (target == "tQDepth") {
+    return TargetMetric::TQDepth;
+  }
   return TargetMetric::Gates;
 }
 } // namespace cs

include/cliffordsynthesis/encoding/GateEncoder.hpp

@@ -30,18 +30,24 @@
     logicbase::LogicMatrix3D gS{};
     // variables for the two-qubit gates
     logicbase::LogicMatrix3D gC{};
+    // variables for the pauli-qubit gates
+    logicbase::LogicMatrix gP{};
 
     void
          collectSingleQubitGateVariables(std::size_t pos, std::size_t qubit,
                                          logicbase::LogicVector& variables) const;
     void collectTwoQubitGateVariables(std::size_t pos, std::size_t qubit,
                                       bool                    target,
                                       logicbase::LogicVector& variables) const;
+    void
+    collectPauliQubitGateVariables(std::size_t             qubit,
+                                   logicbase::LogicVector& variables) const;
   };
 
   // variable creation
-  void createSingleQubitGateVariables();
-  void createTwoQubitGateVariables();
+  virtual void createSingleQubitGateVariables(std::size_t tqEncoding);
+  virtual void createTwoQubitGateVariables(std::size_t tqEncoding);
+  virtual void createPauliQubitGateVariables();
 
   // encode the relation between the tableaus and the gates
   virtual void encodeGates() {
@@ -52,13 +58,20 @@
   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};
+
+  static constexpr std::array<qc::OpType, 4> PAULI_QUBIT_GATES = {
+      qc::OpType::None, qc::OpType::X, qc::OpType::Y, qc::OpType::Z};
 
   [[nodiscard]] static constexpr std::size_t
   gateToIndex(const qc::OpType type) {
@@ -130,9 +143,9 @@
   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 +155,10 @@
   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);

include/cliffordsynthesis/encoding/SATEncoder.hpp

@@ -50,6 +50,12 @@ class SATEncoder {
     // whether to use symmetry breaking
     bool useSymmetryBreaking = false;
 
+    // whether to use SQG-TQG 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;
 

include/cliffordsynthesis/encoding/TwoQubitEncoder.hpp

@@ -0,0 +1,54 @@
+//
+// 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:
+  logicbase::LogicTerm   rChanges{};
+  logicbase::LogicMatrix xorHelpers{};
+
+  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;
+  [[nodiscard]] logicbase::LogicTerm
+  createTwoQubitGateConstraint(std::size_t pos, std::size_t ctrl,
+                               std::size_t trgt) override;
+  [[nodiscard]] logicbase::LogicTerm
+  createIdentityConstraintOnTQG(std::size_t pos, std::size_t ctrl);
+
+  // assert constrains
+  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 collectTwoQubitGateVariables(std::size_t pos, std::size_t qubit,
+                                    bool                    target,
+                                    logicbase::LogicVector& variables) const;
+  // extracting the circuit
+  void extractCircuitFromModel(Results& res, logicbase::Model& model) override;
+
+  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;
+};
+
+} // namespace cs::encoding

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

src/cliffordsynthesis/CliffordSynthesizer.cpp

@@ -5,14 +5,14 @@
 
 #include "cliffordsynthesis/CliffordSynthesizer.hpp"
 
-#include "LogicTerm/Logic.hpp"
 #include "QuantumComputation.hpp"
 #include "cliffordsynthesis/Tableau.hpp"
 #include "utils/logging.hpp"
 
 #include <chrono>
 #include <fstream>
 #include <future>
+#include <iostream>
 #include <memory>
 #include <thread>
 
@@ -44,6 +44,8 @@ void CliffordSynthesizer::synthesize(const Configuration& config) {
   encoderConfig.solverParameters    = configuration.solverParameters;
   encoderConfig.useMultiGateEncoding =
       requiresMultiGateEncoding(encoderConfig.targetMetric);
+  encoderConfig.useTwoQubitEncoding =
+      requiresTwoQubitEncoding(encoderConfig.targetMetric);
 
   if (configuration.heuristic) {
     if (initialCircuit->empty() && !targetTableau.isIdentityTableau()) {
@@ -97,6 +99,9 @@ void CliffordSynthesizer::synthesize(const Configuration& config) {
   case TargetMetric::TwoQubitGates:
     twoQubitGateOptimalSynthesis(encoderConfig, 0U, results.getTwoQubitGates());
     break;
+  case TargetMetric::TQDepth:
+    twoQubitDepthOptimalSynthesis(encoderConfig, lower, upper);
+    break;
   }
 
   results.setSolverCalls(solverCalls);
@@ -130,6 +135,10 @@ void CliffordSynthesizer::determineInitialTimestepLimit(EncoderConfig& config) {
     config.timestepLimit = results.getDepth();
     INFO() << "Using initial circuit's depth as initial timestep limit: "
            << config.timestepLimit;
+  } else if (requiresTwoQubitEncoding(config.targetMetric)) {
+    config.timestepLimit = results.getTQDepth();
+    INFO() << "Using initial circuit's tQDepth as initial timestep limit: "
+           << config.timestepLimit;
   } else {
     config.timestepLimit = results.getGates();
     INFO() << "Using initial circuit's gate count as initial timestep limit: "
@@ -159,6 +168,9 @@ CliffordSynthesizer::determineUpperBound(EncoderConfig config) {
     if (!results.sat()) {
       lowerBound = upperBound + 1U;
       upperBound *= 2U;
+      std::cout << "No solution found for " << config.timestepLimit
+                << " timestep(s). Doubling timestep limit to " << upperBound
+                << std::endl;
       INFO() << "No solution found for " << config.timestepLimit
              << " timestep(s). Doubling timestep limit to " << upperBound;
       config.timestepLimit = upperBound;
@@ -170,6 +182,8 @@ CliffordSynthesizer::determineUpperBound(EncoderConfig config) {
     upperBound = std::min(upperBound, results.getGates());
   } else if (config.targetMetric == TargetMetric::Depth) {
     upperBound = std::min(upperBound, results.getDepth());
+  } else if (config.targetMetric == TargetMetric::TQDepth) {
+    upperBound = std::max(upperBound, results.getTQDepth());
   }
 
   INFO() << "Found upper bound for the number of timesteps: " << upperBound;
@@ -237,6 +251,29 @@ void CliffordSynthesizer::depthOptimalSynthesis(
   }
 }
 
+void CliffordSynthesizer::twoQubitDepthOptimalSynthesis(
+    CliffordSynthesizer::EncoderConfig config, const std::size_t lower,
+    const std::size_t upper) {
+  // tQDepth-optimal synthesis is achieved by determining a timestep limit T
+  // such that there exists a solution with tQDepth T, but no solution with
+  // tQDepth T-1. This procedure uses an encoding (SQG - TQG) where in single
+  // and two qubit gates are allowed just one gate per timestep. This procedure
+  // is guaranteed to produce a depth-optimal circuit. However, the number of
+  // gates in the resulting circuit is not necessarily minimal, i.e., there may
+  // be a solution with fewer gates and the same depth. To this end, an
+  // optimization pass is provided that additionally minimizes the number of
+  // gates.
+
+  if (configuration.linearSearch) {
+    runLinearSearch(config.timestepLimit, lower, upper, config);
+  } else {
+    // The binary search approach calls the SAT solver repeatedly with varying
+    // timestep (=tQDepth) limits T until a solution with tQDepth T is found,
+    // but no solution with tQDepth T-1 could be determined.
+    runBinarySearch(config.timestepLimit, lower, upper, config);
+  }
+}
+
 void CliffordSynthesizer::minimizeGatesFixedDepth(EncoderConfig config) {
   if (results.getDepth() == 0U) {
     return;
@@ -427,6 +464,13 @@ void CliffordSynthesizer::updateResults(const Configuration& config,
       currentResults = newResults;
     }
     break;
+  case TargetMetric::TQDepth:
+    if ((newResults.getTQDepth() < currentResults.getTQDepth()) ||
+        ((newResults.getTQDepth() == currentResults.getTQDepth()) &&
+         (newResults.getGates() < currentResults.getGates()))) {
+      currentResults = newResults;
+    }
+    break;
   }
 }