Approximate equivalence checking

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "extern/mqt-core"]
+	path = extern/mqt-core
+	url = [email protected]:cda-tum/mqt-core.git

cmake/ExternalDependencies.cmake

@@ -65,6 +65,30 @@ if(BUILD_MQT_QCEC_TESTS)
   endif()
 endif()
 
+set(TF_BUILD_TESTS
+    OFF
+    CACHE INTERNAL "")
+set(TF_BUILD_EXAMPLES
+    OFF
+    CACHE INTERNAL "")
+set(TF_BUILD_PROFILER
+    OFF
+    CACHE INTERNAL "")
+set(TF_VERSION
+    3.6.0
+    CACHE STRING "Taskflow version")
+set(TF_URL https://github.com/taskflow/taskflow/archive/refs/tags/v${TF_VERSION}.tar.gz)
+if(CMAKE_VERSION VERSION_GREATER_EQUAL 3.24)
+  FetchContent_Declare(taskflow URL ${TF_URL} FIND_PACKAGE_ARGS)
+  list(APPEND FETCH_PACKAGES taskflow)
+else()
+  find_package(taskflow ${TF_VERSION} QUIET)
+  if(NOT taskflow_FOUND)
+    FetchContent_Declare(taskflow URL ${TF_URL})
+    list(APPEND FETCH_PACKAGES taskflow)
+  endif()
+endif()
+
 if(BUILD_MQT_QCEC_BINDINGS)
   # add pybind11_json library
   if(CMAKE_VERSION VERSION_GREATER_EQUAL 3.24)

docs/source/ApproximateEquivalence.ipynb

@@ -0,0 +1,248 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "77a131e6",
+   "metadata": {},
+   "source": [
+    "# Approximate Equivalence Checking\n",
+    "\n",
+    "## Approximate Equivalence vs. Exact Equivalence\n",
+    "\n",
+    "Two circuits are considered exactly equivalent if their matrix representations, `U` and `V`, are identical. Thus, the problem of exact equivalence checking reduces to verifying whether $UV^\\dagger = I$, where `I` is the identity matrix.\n",
+    "\n",
+    "In practice, however, it is often sufficient to determine whether two circuits are  equivalent up to a certain percentage, while permitting an error tolerance. For instance, when optimizing circuits, we may not require exact equivalence, but rather a circuit that is sufficiently close to the original, while being optimal with respect to a specific metric, such as minimizing gate counts.\n",
+    "\n",
+    "Here, approximate equivalence is quantified by the process distance between two circuits based on the Hilbert-Schmidt inner product, with n being the number of qubits: $$\\Delta(U, V) = 1 - |\\frac{Tr(U V^\\dagger)}{2^n}|$$ Specifically, we compute the magnitude of the normalized trace of $UV^\\dagger$ and assess its proximity to 1. Two circuits are considered approximately equivalent if their process distance is below a specified error threshold, $\\epsilon$.\n",
+    "\n",
+    "\n",
+    "\n",
+    "\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "b9be796e",
+   "metadata": {},
+   "source": [
+    "\n",
+    "## Checking Approximate Equivalence of Quantum Circuits\n",
+    "\n",
+    "To enable approximate equivalence checking, set the `check_approximate_equivalence` option to `True` in the configuration parameters. When activated, the equivalence checker will return `equivalent` if the process distance is below a specified threshold. Otherwise, it will return `not-equivalent`. The error threshold is controlled via the `approximate_checking_threshold` parameter, with a default value of `1e-8`. Moreover, it is recommended to disable the simulation checker by setting `run_simulation_checker` to `False`.\n",
+    "\n",
+    "The following is a summary of the behaviour of each type of equivalence checker when the `checkApproximateEquivalence` option is set to `True`.\n",
+    "\n",
+    "1. **Construction Equivalence Checker:** The construction checker supports approximate equivalence checking by using decision diagrams to compute $UV^\\dagger$. It then calculates the normalized trace and compares the process distance to the defined error threshold. \n",
+    "\n",
+    "1. **Alternating Equivalence Checker:** The alternating checker likewise computes the composition of one circuit with the inverse of the other. Again, when checking for approximate equivalence, it suffices to verify that the normalized trace is sufficiently close to 1. \n",
+    "\n",
+    "1. **Simulation Equivalence Checker:** Approximate equivalence checking is not directly supported by the Simulation checker. Although numerical instabilities can be mitigated through the configuration parameter `simulation.fidelityThreshold`, this parameter does not serve as an approximate equivalence threshold. For instance, consider $UV^\\dagger$ representing a 10-qubit multi-controlled X-gate with the first 9 qubits as control and the last qubit as the target. In this setup, the process distance would meet an error threshold of $1e^-2$. However, since the Simulation checker evaluates both circuits using random input states, the fidelity drops to zero whenever one of the two computational basis states, $|1111111110\\rangle$ or $|1111111111\\rangle$, is selected. In such cases, regardless of any threshold setting, the checker reports non-equivalence.\n",
+    "\n",
+    "1. **ZX-Calculus Equivalence Checker:** Approximate equivalence checking is not yet supported in the ZX-calculus checker, which is not a problem for the equivalence checking workflow, 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 approximately but not totally equivalent.\n",
+    "\n",
+    "1. **Hybrid Schrödinger-Feynman (HSF) Equivalence Checker:** By default, the HSF checker is disabled. It can only be used for approximate equivalence checking. To enable it, the `check_approximate_equivalence` option must also be activated. The HSF checker computes the process distance by dividing the circuit corresponding to $UV^\\dagger$ horizontally into two independent halves: a lower part and an upper part. This is achieved by decomposing controlled gates, acting across both halves, according to the Schmidt decomposition.\n",
+    "By leveraging key trace equalities - specifically,\n",
+    "\n",
+    "    • $tr[L⊗U]=tr[L]⋅tr[U]$\n",
+    "\n",
+    "    • $tr[P_1+P_2]=tr[P_1]+tr[P_2]$\n",
+    "\n",
+    "    we can treat the lower and upper circuit parts, as well as the summands from the Schmidt decomposition, independently. This enables parallel trace computation, allowing to check the equivalence of larger, yet shallow circuits.\n",
+    "    \n",
+    "    Note: The following configurations are not currently supported, as they require the explicit computation of the Schmidt decomposition for the gates being cut (decisions):\n",
+    "\n",
+    "        • Multiple targets spread across the cut through the circuit\n",
+    "        • Multiple controls in the control part of the gate being cut \n",
+    "    \n",
+    "    Moreover, despite parallelization, the method is best suited for shallow circuits, as the number of paths to be computed grows exponentially with the number of decisions. "
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "977071d9",
+   "metadata": {},
+   "source": [
+    "## Using QCEC to Check for Approximate Equivalence\n",
+    "\n",
+    "Consider the following three-qubit circuit representing the Toffoli gate."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "03b73b17",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from qiskit import QuantumCircuit\n",
+    "\n",
+    "qc_lhs = QuantumCircuit(3)\n",
+    "qc_lhs.mcx([0, 1], 2)\n",
+    "qc_lhs.measure_all()\n",
+    "qc_lhs.draw(output=\"mpl\", style=\"iqp\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "10fff8c7-f36c-422e-8deb-796cc7637e45",
+   "metadata": {},
+   "source": [
+    "Additionally, consider the following simple circuit, which represents the Identity."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "d167869e-e082-4a42-9eab-112931f5c697",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "qc_rhs = QuantumCircuit(3)\n",
+    "qc_rhs.id(0)\n",
+    "qc_rhs.id(1)\n",
+    "qc_rhs.id(2)\n",
+    "qc_rhs.measure_all()\n",
+    "qc_rhs.draw(output=\"mpl\", style=\"iqp\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "3b85338e",
+   "metadata": {},
+   "source": [
+    "We now aim to compute the process distance between these circuits. Since the second circuit represents the Identity, it follows that $UV^\\dagger$ simplifies to the Toffoli gate matrix. \n",
+    "\n",
+    "$$\n",
+    "\\text{Toffoli} = \\begin{bmatrix}\n",
+    "1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 \\\\\n",
+    "0 & 1 & 0 & 0 & 0 & 0 & 0 & 0 \\\\\n",
+    "0 & 0 & 1 & 0 & 0 & 0 & 0 & 0 \\\\\n",
+    "0 & 0 & 0 & 1 & 0 & 0 & 0 & 0 \\\\\n",
+    "0 & 0 & 0 & 0 & 1 & 0 & 0 & 0 \\\\\n",
+    "0 & 0 & 0 & 0 & 0 & 1 & 0 & 0 \\\\\n",
+    "0 & 0 & 0 & 0 & 0 & 0 & 0 & 1 \\\\\n",
+    "0 & 0 & 0 & 0 & 0 & 0 & 1 & 0 \\\\\n",
+    "\\end{bmatrix}\n",
+    "$$\n",
+    "\n",
+    "The normalized trace of this matrix is `0.75`. \n",
+    "\n",
+    "Consequently, the process distance $\\Delta(U, V) = 1 - |\\frac{Tr(U V^\\dagger)}{2^n}|$ is equal to `0.25`.\n",
+    "\n",
+    "If we set the equivalence tolerance to `0.3`, the checker should output `equivalent`."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "36df44b7",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from mqt.qcec import Configuration, verify\n",
+    "\n",
+    "config = Configuration()\n",
+    "config.execution.run_simulation_checker = False\n",
+    "config.functionality.check_approximate_equivalence = True\n",
+    "config.functionality.approximate_checking_threshold = 0.3\n",
+    "verify(qc_lhs, qc_rhs, configuration=config)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "f2c4104d",
+   "metadata": {},
+   "source": [
+    "However, with an error tolerance below `0.25`, the checker should return `not_equivalent`."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "da9fa188",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "config = Configuration()\n",
+    "config.execution.run_simulation_checker = False\n",
+    "config.functionality.check_approximate_equivalence = True\n",
+    "config.functionality.approximate_checking_threshold = 0.2\n",
+    "verify(qc_lhs, qc_rhs, configuration=config)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "5d7f9c62",
+   "metadata": {},
+   "source": [
+    "To use the HSF checker, it must be explicitly enabled in the configuration. Below, we will explicitly use the HSF checker and disable the other checkers."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "494ef477",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "config.execution.run_simulation_checker = False\n",
+    "config.execution.run_alternating_checker = False\n",
+    "config.execution.run_construction_checker = False\n",
+    "config.execution.run_zx_checker = False\n",
+    "config.execution.run_hsf_checker = True\n",
+    "config.functionality.check_approximate_equivalence = False\n",
+    "config.functionality.approximate_checking_threshold = 0.3\n",
+    "verify(qc_lhs, qc_rhs, configuration=config)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "b327ab4b",
+   "metadata": {},
+   "source": [
+    "However, we also need to explicitly enable the `check_approximate_equivalence` option."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "679291b7",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "config.functionality.check_approximate_equivalence = True\n",
+    "config.functionality.approximate_checking_threshold = 0.3\n",
+    "verify(qc_lhs, qc_rhs, configuration=config)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "6af54b68",
+   "metadata": {},
+   "source": [
+    "Source: The concept of approximate equivalence used here is inspired by [Approximate Equivalence Checking of Noisy Quantum Circuits](https://arxiv.org/abs/2103.11595) by Xin Hong, Mingsheng Ying, Yuan Feng, Xiangzhen Zhou, Sanjiang Li, and [QUEST: systematically approximating Quantum circuits for higher output fidelity](https://dl.acm.org/doi/10.1145/3503222.3507739) by Tirthak Patel, Ed Younis, Costin Iancu, Wibe de Jong, and Devesh Tiwari."
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "venv",
+   "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

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

include/Configuration.hpp

@@ -33,6 +33,7 @@ class Configuration {
     bool runSimulationChecker = true;
     bool runAlternatingChecker = true;
     bool runZXChecker = true;
+    bool runHSFChecker = false;
   };
 
   // configuration options for pre-check optimizations
@@ -62,7 +63,9 @@ class Configuration {
 
   struct Functionality {
     double traceThreshold = 1e-8;
+    double approximateCheckingThreshold = 1e-8;
     bool checkPartialEquivalence = false;
+    bool checkApproximateEquivalence = false;
   };
 
   // configuration options for the simulation scheme

include/EquivalenceCheckingManager.hpp

@@ -139,12 +139,14 @@ class EquivalenceCheckingManager {
     configuration.execution.runAlternatingChecker = run;
   }
   void setZXChecker(bool run) { configuration.execution.runZXChecker = run; }
+  void setHSFChecker(bool run) { configuration.execution.runHSFChecker = run; }
 
   void disableAllCheckers() {
     configuration.execution.runConstructionChecker = false;
     configuration.execution.runZXChecker = false;
     configuration.execution.runSimulationChecker = false;
     configuration.execution.runAlternatingChecker = false;
+    configuration.execution.runHSFChecker = false;
   }
 
   // Optimization: Optimizations are applied during initialization. Already
@@ -219,10 +221,16 @@ class EquivalenceCheckingManager {
   void setTraceThreshold(double traceThreshold) {
     configuration.functionality.traceThreshold = traceThreshold;
   }
+  void setApproximateCheckingThreshold(double approximateCheckingThreshold) {
+    configuration.functionality.approximateCheckingThreshold =
+        approximateCheckingThreshold;
+  }
   void setCheckPartialEquivalence(bool checkPE) {
     configuration.functionality.checkPartialEquivalence = checkPE;
   }
-
+  void setCheckApproximateEquivalence(bool checkAE) {
+    configuration.functionality.checkApproximateEquivalence = checkAE;
+  }
   // Simulation: These setting may be changed to adjust the kinds of simulations
   // that are performed
   void setFidelityThreshold(double fidelityThreshold) {