Merge branch 'main' into msoeken/re-update

.github/workflows/coverage.yml

@@ -17,7 +17,7 @@ jobs:
         with:
           python-version: "3.9"
       - name: Install MQT ProblemSolver
-        run: pip install .[coverage]
+        run: pip install .[coverage,tweedledum]
       - name: Generate Report
         run: pytest -v --cov --cov-config=pyproject.toml --cov-report=xml
       - name: Upload coverage to Codecov

.pre-commit-config.yaml

@@ -89,3 +89,4 @@ repos:
           - networkx
           - mqt.ddsim
           - pytest
+          - pandas-stubs

README.md

@@ -18,6 +18,7 @@ This repository covers the implementations of multiple research papers in the do
 2. [A Hybrid Classical Quantum Computing Approach to the Satellite Mission Planning Problem](#a-hybrid-classical-quantum-computing-approach-to-the-satellite-mission-planning-problem)
 3. [Reducing the Compilation Time of Quantum Circuits Using Pre-Compilation on the Gate Level](#reducing-the-compilation-time-of-quantum-circuits-using-pre-compilation-on-the-gate-level)
 4. [Utilizing Resource Estimation for the Development of Quantum Computing Applications](#utilizing-resource-estimation-for-the-development-of-quantum-computing-applications)
+5. [Towards Equivalence Checking of Classical Circuits Using Quantum Computing](#towards-equivalence-checking-of-classical-circuits-using-quantum-computing)
 
 In the following, each implementation is briefly introduced.
 
@@ -117,6 +118,21 @@ In this evaluation, we investigate
 - different design trade-offs, and
 - hypothesis on how quantum hardware might improve and how it affects the required resources.
 
+# Towards Equivalence Checking of Classical Circuits Using Quantum Computing
+
+Equivalence checking, i.e., verifying whether two circuits realize the same functionality or not, is a typical task in the semiconductor industry. Due to the fact, that the designs grow faster than the ability to efficiently verify them, all alternative directions to close the resulting verification gap should be considered. In this work, we consider the problem through the miter structure. Here, two circuits to be checked are applied with the same primary inputs. Then, for each pair of to-be-equal output bits, an exclusive-OR (XOR) gate is applied-evaluating to 1 if the two outputs generate different values (which only happens in the case of non-equivalence). By OR-ing the outputs of all these XOR gates, eventually an indicator results that shows whether both circuits are equivalent. Then, the goal is to determine an input assignment so that this indicator evaluates to 1 (providing a counter example that shows non-equivalence) or to prove that no such assignment exists (proving equivalence).
+
+<p align="center">
+<img src="img/miter_structure.png" height=250px>
+</p>
+
+In the `equivalence_checking` module, our approach to this problem by utilizing quantum computing is implemented. There are two different ways to run this code.
+
+- One to test, how well certain parameter combinations work. The parameters consist of the number of bits of the circuits to be verified, the threshold parameter delta (which is explained in detail in the paper), the fraction of input combinations that induce non-equivalence of the circuits (further called "counter examples"), the number of shots to run the quantum circuit for and the number of individual runs of the experiment. Multiple parameter combinations can be tested and exported as a .csv-file at a provided location.
+- A second one to actually input a miter expression (in form of a string) together with some parameters independent from the miter (shots and delta) and use our approach to find the counter examples (if the circuits are non-equivalent).
+
+These two implementations are provided by the functions `try_parameter_combinations()` and `find_counter_examples()`, respectively. Examples for their usages are shown in `notebooks/equivalence_checking/example.ipynb`.
+
 # Usage
 
 MQT ProblemSolver is available via [PyPI](https://pypi.org/project/mqt.problemsolver/):
@@ -191,6 +207,20 @@ In case you are using our Resources Estimation approach, we would be thankful if
 which is also available on arXiv:
 [![a](https://img.shields.io/static/v1?label=arXiv&message=2402.12434&color=inactive&style=flat-square)](https://arxiv.org/abs/2402.12434)
 
+In case you are using our Equivalence-Checking approach, we would be thankful if you referred to it by citing the following publication:
+
+```bibtex
+@INPROCEEDINGS{quetschlich2024equivalence_checking,
+    title     = {{Towards Equivalence Checking of Classical Circuits Using Quantum Computing}},
+    author    = {N. Quetschlich and T. Forster and A. Osterwind and D. Helms and R. Wille},
+    booktitle = {IEEE International Conference on Quantum Computing and Engineering (QCE)},
+    year      = {2024},
+}
+```
+
+which is also available on arXiv:
+[![a]()
+
 ## Acknowledgements
 
 This project received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research

notebooks/equivalence_checking/equivalence_checking_example.ipynb

@@ -0,0 +1,102 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Import"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": []
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from mqt.problemsolver.equivalence_checking import equivalence_checking"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Testing different Parameter Combinations for a Miter with known Counter Examples"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "# Generate table with all possible parameter combinations\n",
+    "# that shows the used Grover iterations if correct counter examples\n",
+    "# are found in all runs.\n",
+    "equivalence_checking.try_parameter_combinations(\n",
+    "    path=\"res_equivalence_checking.csv\",  # Path to save the results\n",
+    "    range_deltas=[0.1, 0.3, 0.5, 0.7, 0.9],  # Range of \"delta\" values, a threshold parameter introduced in the paper\n",
+    "    range_num_bits=[6, 7, 8, 9],  # Range of number of bits of the circuits to be verified\n",
+    "    range_fraction_counter_examples=[0, 0.01, 0.05, 0.1, 0.2],  # Range of fraction of counter examples to be used\n",
+    "    shots_factor=8.0,  # The number of shots for the quantum circuit is calculated as shots_factor * 2^num_bits\n",
+    "    num_runs=10,  # Number of individual runs for each parameter combination\n",
+    "    verbose=False,  # If True, the progress is printed\n",
+    ")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Find Counter Examples for given Miter and Parameter Combination"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "num_bits = 6\n",
+    "num_counter_examples = 5\n",
+    "\n",
+    "# Create synthetic data for showing the example\n",
+    "miter, _ = equivalence_checking.create_condition_string(num_bits=num_bits, num_counter_examples=num_counter_examples)\n",
+    "\n",
+    "# Run the equivalence checker\n",
+    "counter_examples = equivalence_checking.find_counter_examples(\n",
+    "    miter=miter,  # The condition string\n",
+    "    num_bits=num_bits,  # Number of bits of the circuits to be verified\n",
+    "    shots=512,  # Number of shots for the quantum circuit\n",
+    "    delta=0.7,  # Threshold parameter introduced in the paper\n",
+    ")\n",
+    "\n",
+    "print(counter_examples)"
+   ]
+  }
+ ],
+ "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": 2
+}

notebooks/equivalence_checking/res_equivalence_checking.csv

@@ -0,0 +1,21 @@
+Input Bits,Counter Examples,0.1,0.3,0.5,0.7,0.9
+6.0,0.0,-,15.0,15.0,15.0,15.0
+6.0,1.0,5.0,5.0,5.0,5.0,5.0
+6.0,3.0,-,5.0,5.0,5.0,9.0
+6.0,6.0,-,12.0,12.0,12.0,14.0
+6.0,13.0,-,5.0,5.0,5.0,-
+7.0,0.0,-,36.0,36.0,36.0,36.0
+7.0,1.0,8.0,8.0,8.0,8.0,8.0
+7.0,6.0,-,8.0,8.0,17.0,30.0
+7.0,13.0,-,8.0,9.0,15.0,15.0
+7.0,26.0,-,8.0,8.0,8.0,8.0
+8.0,0.0,-,78.0,78.0,78.0,78.0
+8.0,3.0,-,12.0,12.0,12.0,23.0
+8.0,13.0,-,12.0,12.0,22.0,23.0
+8.0,26.0,-,12.0,12.0,12.0,12.0
+8.0,51,-,12.0,20.0,23.0,50.0
+9.0,0.0,-,153.0,153.0,153.0,153.0
+9.0,5.0,-,17.0,17.0,17.0,80.0
+9.0,26.0,-,17.0,17.0,17.0,17.0
+9.0,51.0,-,17.0,17.0,17.0,17.0
+9.0,102.0,-,48.0,48.0,48.0,-

notebooks/precompilation/evaluation.ipynb

@@ -15,6 +15,8 @@
    "metadata": {},
    "outputs": [],
    "source": [
+    "from __future__ import annotations\n",
+    "\n",
     "import pandas as pd\n",
     "\n",
     "%matplotlib inline\n",

pyproject.toml

@@ -27,7 +27,9 @@ dependencies = [
     "networkx",
     "python_tsp",
     "docplex",
-    "qiskit_optimization"
+    "qiskit_optimization",
+    "qiskit_aer",
+    "pandas"
 ]
 
 classifiers = [
@@ -51,6 +53,7 @@ classifiers = [
 test = ["pytest>=7"]
 coverage = ["mqt.problemsolver[test]", "coverage[toml]~=6.5.0", "pytest-cov~=4.0.0"]
 dev = ["mqt.problemsolver[coverage]"]
+tweedledum = ["tweedledum==1.0.0"]
 
 [project.urls]
 Homepage = "https://github.com/cda-tum/mqtproblemsolver"
@@ -81,7 +84,7 @@ explicit_package_bases = true
 pretty = true
 
 [[tool.mypy.overrides]]
-module = ["qiskit.*",  "matplotlib.*", "python_tsp.*", "networkx.*", "mqt.ddsim.*", "joblib.*", "qiskit_optimization.*", "docplex.*"]
+module = ["qiskit.*",  "matplotlib.*", "python_tsp.*", "networkx.*", "mqt.ddsim.*", "joblib.*", "qiskit_optimization.*", "docplex.*", "qiskit_aer.*"]
 ignore_missing_imports = true
 
 [tool.ruff]