✨ Partial equivalence checking

.gitmodules

@@ -1,4 +1,4 @@
 [submodule "extern/mqt-core"]
-	path = extern/mqt-core
+    path = extern/mqt-core
     url = https://github.com/cda-tum/mqt-core.git
     branch = main

docs/source/PartialEquivalence.ipynb

@@ -0,0 +1,192 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "77a131e6",
+   "metadata": {},
+   "source": [
+    "# Partial Equivalence Checking\n",
+    "\n",
+    "## Partial Equivalence vs. Total Equivalence\n",
+    "\n",
+    "Different definitions of quantum circuit equivalence have been proposed, with the most commonly used being total equivalence. \n",
+    "Two circuits are considered totally equivalent when their matrix representations are exactly the same. \n",
+    "However, it is often sufficient to consider observational equivalence, because the only way to extract information from a quantum circuit is through measurement. \n",
+    "Therefore, partial equivalence has been defined, which is a weaker equality than total equivalence. \n",
+    "Two circuits are considered partially equivalent if, for each possible input state, they have the same probabilities for each measurement outcome. \n",
+    "In particular, partial equivalence doesn't consider qubits that are not measured or different phase angles for each measurement.\n",
+    "\n",
+    "This definition is especially useful for circuits that do not measure all of their qubits at the end, or where some qubits are initialized to a certain value at the beginning. \n",
+    "We refer to the qubits that are initialized to a certain value at the beginning of the computation as *ancillary* qubits. \n",
+    "Without loss of generality, we assume that these qubits are initially set to $|0\\rangle$. \n",
+    "Any other initial state can be reached from the $|0\\rangle$ state by applying the appropriate gates. \n",
+    "The remaining qubits are the qubits that hold the input state, and they are referred to as *data* qubits.\n",
+    "\n",
+    "Similarly, we differentiate between *measured* and *garbage* qubits. \n",
+    "In order to read the output at the end of a circuit, a measurement is performed on some qubits, but not necessarily all of them. \n",
+    "These qubits are the *measured* qubits. All qubits that are not measured are called the *garbage* qubits. \n",
+    "Their final state doesn't influence the output we obtain from the computation. \n",
+    "\n",
+    "For a circuit $C$ we denote $P(t | \\psi, C)$ as the probability that the quantum circuit $C$ collapses to state $|t\\rangle$ upon a measurement on the measured qubits, \n",
+    "given that the data qubits have the initial state $|\\psi\\rangle$. \n",
+    "Two circuits $C_1$ and $C_2$ are considered partially equivalent if, for each initial state $|\\psi\\rangle$ of the data qubits and each final state $|t\\rangle$ of the measured qubits, \n",
+    "it holds that $P(t|\\psi, C_1) = P(t|\\psi, C_2)$.\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "b9be796e",
+   "metadata": {},
+   "source": [
+    "\n",
+    "## Checking Partial Equivalence of Quantum Circuits\n",
+    "\n",
+    "Partial equivalence checking is a bit more costly than regular equivalence checking. \n",
+    "It is necessary to reduce the contribution of garbage qubits and normalize the phase of each measurement outcome. \n",
+    "Therefore, it is not enabled by default in QCEC. \n",
+    "It can be activated using an option in the configuration parameters. \n",
+    "If the option `check_partial_equivalence` is set to `True`, the equivalence checker will return `equivalent` not only for totally equivalent circuits, \n",
+    "but also for partially equivalent circuits. The result will be `not_equivalent` if and only if the circuits are not partially equivalent. \n",
+    "On the other hand, if the option `check_partial_equivalence` is set to `False`, then the equivalence checker considers total equivalence modulo ancillary qubits. \n",
+    "This means that the garbage qubits are considered as if they were measured qubits, while ancillary qubits are set to zero, as in the partial equivalence check. \n",
+    "The equivalence checker will return `equivalent` for totally equivalent circuits or `equivalent_up_to_global_phase` for circuits which differ only in their global phase \n",
+    "and `not_equivalent` for other circuits.\n",
+    "\n",
+    "The following is a summary of the behaviour of each type of equivalence checker when the `check_partial_equivalence` option is set to `True`.\n",
+    "\n",
+    "1. **Construction Equivalence Checker:** The construction checker supports partial equivalence checking by using decision diagrams to calculate the normalized phases of the possible outputs and then summing up the contribution of garbage qubits, in order to consider only the measurement probabilities of measured qubits. \n",
+    "Then it compares the reduced decision diagrams of the two circuits. \n",
+    "\n",
+    "1. **Alternating Equivalence Checker:** The alternating checker can only be used for circuits where at least one of the two does not contain ancillary qubits. \n",
+    "It computes the composition of one circuit with the inverse of the other and verifies that the result resembles the identity. \n",
+    "When checking for partial equivalence, it suffices to verify that the result resembles the identity modulo garbage qubits. \n",
+    "\n",
+    "1. **Simulation Equivalence Checker:** The simulation checker computes a representation of the state vector resulting from simulating the circuit with certain initial states. \n",
+    "Partial equivalence is enabled by summing up the contributions of garbage qubits.\n",
+    "\n",
+    "1. **ZX-Calculus Equivalence Checker:** The ZX-calculus checker doesn't directly support partial equivalence, which is not a problem for the equivalence checking workflow, \n",
+    "given that the ZX-calculus checker cannot demonstrate non-equivalence of circuits due to its incompleteness. \n",
+    "Therefore it will simply output 'No Information' for circuits that are partially but not totally equivalent."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "977071d9",
+   "metadata": {},
+   "source": [
+    "## Using QCEC to Check for Partial Equivalence\n",
+    "\n",
+    "Consider the following quantum circuit with three qubits, which are all data qubits, but only one of them is measured."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "03b73b17",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from qiskit import QuantumCircuit\n",
+    "\n",
+    "qc_lhs = QuantumCircuit(3, 1)\n",
+    "qc_lhs.cswap(1, 0, 2)\n",
+    "qc_lhs.h(0)\n",
+    "qc_lhs.z(2)\n",
+    "qc_lhs.cswap(1, 0, 2)\n",
+    "qc_lhs.measure(0, 0)\n",
+    "\n",
+    "qc_lhs.draw(output=\"mpl\", style=\"iqp\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "10fff8c7-f36c-422e-8deb-796cc7637e45",
+   "metadata": {},
+   "source": [
+    "Aditionally, consider the following circuit, which only acts on two qubits."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "d167869e-e082-4a42-9eab-112931f5c697",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "qc_rhs = QuantumCircuit(3, 1)\n",
+    "qc_rhs.x(1)\n",
+    "qc_rhs.ch(1, 0)\n",
+    "qc_rhs.measure(0, 0)\n",
+    "qc_rhs.draw(output=\"mpl\", style=\"iqp\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "3b85338e",
+   "metadata": {},
+   "source": [
+    "Then, these circuits are not totally equivalent, as can be shown using QCEC. \n",
+    "The library even emits a handy warning in this case that indicates that two circuits have been shown to be non-equivalent, but at least one of the circuits does not measure all its qubits (i.e., has garbage qubits) and partial equivalence checking support has not been enabled."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "36df44b7",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from mqt.qcec import verify\n",
+    "\n",
+    "verify(qc_lhs, qc_rhs)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "8cae4862",
+   "metadata": {},
+   "source": [
+    "However, both circuits are partially equivalent, because they have the same probability distribution of measured values for any given initial input state.\n",
+    "This equality can be proven with QCEC by enabling the `check_partial_equivalence` option:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "da9fa188",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "verify(qc_lhs, qc_rhs, check_partial_equivalence=True)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "6af54b68",
+   "metadata": {},
+   "source": [
+    "Source: The definitions and example for partial equivalence are described in the paper [Partial Equivalence Checking of Quantum Circuits](https://arxiv.org/abs/2208.07564) by Tian-Fu Chen, Jie-Hong R. Jiang and Min-Hsiu Hsieh."
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3 (ipykernel)",
+   "language": "python",
+   "name": "python3"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}

docs/source/index.rst

@@ -26,6 +26,7 @@ We appreciate any feedback and contributions to the project. If you want to cont
     EquivalenceChecking
     CompilationFlowVerification
     ParameterizedCircuits
+    PartialEquivalence
     Publications
 
  .. toctree::

include/Configuration.hpp

@@ -57,7 +57,8 @@ class Configuration {
   };
 
   struct Functionality {
-    double traceThreshold = 1e-8;
+    double traceThreshold          = 1e-8;
+    bool   checkPartialEquivalence = false;
   };
 
   // configuration options for the simulation scheme
@@ -186,8 +187,9 @@ class Configuration {
     par["additional_instantiations"] = parameterized.nAdditionalInstantiations;
 
     if (execution.runConstructionChecker || execution.runAlternatingChecker) {
-      auto& fun              = config["functionality"];
-      fun["trace_threshold"] = functionality.traceThreshold;
+      auto& fun                        = config["functionality"];
+      fun["trace_threshold"]           = functionality.traceThreshold;
+      fun["check_partial_equivalence"] = functionality.checkPartialEquivalence;
     }
 
     if (execution.runSimulationChecker) {

include/EquivalenceCheckingManager.hpp

@@ -196,6 +196,9 @@ class EquivalenceCheckingManager {
   void setTraceThreshold(double traceThreshold) {
     configuration.functionality.traceThreshold = traceThreshold;
   }
+  void setCheckPartialEquivalence(bool checkPE) {
+    configuration.functionality.checkPartialEquivalence = checkPE;
+  }
 
   // Simulation: These setting may be changed to adjust the kinds of simulations
   // that are performed

include/checker/dd/TaskManager.hpp

@@ -113,12 +113,16 @@ template <class DDType, class Config = dd::DDPackageConfig> class TaskManager {
   }
   void reduceAncillae() { reduceAncillae(internalState); }
 
+  /**
+   Reduces garbage qubits such that the matrix will be equal to another reduced
+   matrix iff the two underlying circuits are partially equivalent.
+   **/
   void reduceGarbage(DDType& state) {
     if constexpr (std::is_same_v<DDType, qc::VectorDD>) {
-      state = package->reduceGarbage(state, qc->garbage);
+      state = package->reduceGarbage(state, qc->garbage, true);
     } else if constexpr (std::is_same_v<DDType, qc::MatrixDD>) {
       state = package->reduceGarbage(state, qc->garbage,
-                                     static_cast<bool>(direction));
+                                     static_cast<bool>(direction), true);
     }
   }
   void reduceGarbage() { reduceGarbage(internalState); }

src/EquivalenceCheckingManager.cpp

@@ -156,6 +156,8 @@ void EquivalenceCheckingManager::runOptimizationPasses() {
 void EquivalenceCheckingManager::run() {
   done                = false;
   results.equivalence = EquivalenceCriterion::NoInformation;
+  bool garbageQubitsPresent =
+      qc1.getNgarbageQubits() > 0 || qc2.getNgarbageQubits() > 0;
 
   if (!configuration.anythingToExecute()) {
     std::clog << "Nothing to be executed. Check your configuration!\n";
@@ -179,6 +181,16 @@ void EquivalenceCheckingManager::run() {
   } else {
     checkSymbolic();
   }
+
+  if (!configuration.functionality.checkPartialEquivalence &&
+      garbageQubitsPresent &&
+      equivalence() == EquivalenceCriterion::NotEquivalent) {
+    std::clog << "[QCEC] Warning: at least one of the circuits has garbage "
+                 "qubits, but partial equivalence checking is turned off. In "
+                 "order to take into account the garbage qubits, enable partial"
+                 " equivalence checking. Consult the documentation for more"
+                 "information.\n";
+  }
 }
 
 EquivalenceCheckingManager::EquivalenceCheckingManager(

src/checker/dd/DDAlternatingChecker.cpp

@@ -101,11 +101,13 @@ EquivalenceCriterion DDAlternatingChecker::checkEquivalence() {
     garbage[static_cast<std::size_t>(q)] =
         qc1.logicalQubitIsGarbage(q) && qc2.logicalQubitIsGarbage(q);
   }
-
-  // if partial equivalence is being checked instead of total equivalence, it
-  // suffices to change the last parameter of isCloseToIdentity to `false`
-  const bool isClose = dd->isCloseToIdentity(
-      functionality, configuration.functionality.traceThreshold, garbage, true);
+  bool isClose =
+      configuration.functionality.checkPartialEquivalence
+          ? dd->isCloseToIdentity(functionality,
+                                  configuration.functionality.traceThreshold,
+                                  garbage, false)
+          : dd->isCloseToIdentity(functionality,
+                                  configuration.functionality.traceThreshold);
 
   if (isClose) {
     // whenever the top edge weight is not one, both decision diagrams are only

src/checker/dd/DDEquivalenceChecker.cpp

@@ -203,8 +203,11 @@ void DDEquivalenceChecker<DDType, Config>::postprocessTask(
   if (isDone()) {
     return;
   }
-  // sum up the contributions of garbage qubits
-  task.reduceGarbage();
+  // sum up the contributions of garbage qubits if we want to check for partial
+  // equivalence
+  if (configuration.functionality.checkPartialEquivalence) {
+    task.reduceGarbage();
+  }
 }
 
 template <class DDType, class Config>

src/mqt/qcec/configuration.py

@@ -32,6 +32,7 @@ class ConfigurationOptions(TypedDict, total=False):
     timeout: float
     # Functionality
     trace_threshold: float
+    check_partial_equivalence: bool
     # Optimizations
     backpropagate_output_permutation: bool
     fix_output_permutation_mismatch: bool

src/mqt/qcec/pyqcec.pyi

@@ -48,6 +48,7 @@ class Configuration:
 
     class Functionality:
         trace_threshold: float
+        check_partial_equivalence: bool
         def __init__(self) -> None: ...
 
     class Optimizations:
@@ -132,6 +133,7 @@ class EquivalenceCheckingManager:
     def set_timeout(self, timeout: float = ...) -> None: ...
     def set_tolerance(self, tolerance: float = ...) -> None: ...
     def set_trace_threshold(self, threshold: float = ...) -> None: ...
+    def set_check_partial_equivalence(self, enable: bool = ...) -> None: ...
     def set_zx_checker(self, enable: bool = ...) -> None: ...
     def store_cex_input(self, enable: bool = ...) -> None: ...
     def store_cex_output(self, enable: bool = ...) -> None: ...

src/python/bindings.cpp

@@ -313,6 +313,15 @@ PYBIND11_MODULE(pyqcec, m) {
            "Set the :attr:`trace threshold "
            "<.Configuration.Functionality.trace_threshold>` used for comparing "
            "two unitaries or functionality matrices.")
+      .def(
+          "set_check_partial_equivalence",
+          &EquivalenceCheckingManager::setCheckPartialEquivalence,
+          "enable"_a = false,
+          "Set whether to check for partial equivalence. Two circuits are "
+          "partially equivalent if, for each possible initial input state, "
+          "they have the same probability for each measurement outcome. "
+          "If set to false, the checker will output 'not equivalent' for "
+          "circuits that are partially equivalent but not totally equivalent. ")
       // Simulation
       .def("set_fidelity_threshold",
            &EquivalenceCheckingManager::setFidelityThreshold,
@@ -612,7 +621,19 @@ PYBIND11_MODULE(pyqcec, m) {
           "while the second and third successor have weights close to zero). "
           "Whenever any decision diagram node differs from this structure by "
           "more than the configured threshold, the circuits are concluded to "
-          "be non-equivalent. Defaults to :code:`1e-8`.");
+          "be non-equivalent. Defaults to :code:`1e-8`.")
+      .def_readwrite(
+          "check_partial_equivalence",
+          &Configuration::Functionality::checkPartialEquivalence,
+          "Two circuits are partially equivalent if, for each possible initial "
+          "input state, they have the same probability for each measurement "
+          "outcome. If set to :code:`True`, a check for partial equivalence "
+          "will be performed and the contributions of garbage qubits to the "
+          "circuit are ignored. If set to :code:`False`, the checker will "
+          "output 'not equivalent' for circuits that are partially equivalent "
+          "but not totally equivalent. In particular, garbage qubits will be "
+          "treated as if they were measured qubits. Defaults to "
+          ":code:`False`.");
 
   // simulation options
   simulation.def(py::init<>())