MQT ProblemSolver

This repository covers the implementations of multiple research papers in the domain of quantum computing:

Towards an Automated Framework for Realizing Quantum Computing Solutions
A Hybrid Classical Quantum Computing Approach to the Satellite Mission Planning Problem
Reducing the Compilation Time of Quantum Circuits Using Pre-Compilation on the Gate Level
Utilizing Resource Estimation for the Development of Quantum Computing Applications
Towards Equivalence Checking of Classical Circuits Using Quantum Computing

In the following, each implementation is briefly introduced.

Towards an Automated Framework for Realizing Quantum Computing Solutions

MQT ProblemSolver provides a framework to utilize quantum computing as a technology for users with little to no quantum computing knowledge that is part of the Munich Quantum Toolkit (MQT) developed by the Chair for Design Automation at the Technical University of Munich. All necessary quantum parts are embedded by domain experts while the interfaces provided are similar to the ones classical solver provide:

When provided with a problem description, MQT ProblemSolver offers a selection of implemented quantum algorithms. The user just has to chose one and all further (quantum) calculation steps are encapsulated within MQT ProblemSolver. After the calculation finished, the respective solution is returned - again in the same format as classical solvers use.

In the current implementation, two case studies are conducted:

A SAT Problem: Constraint Satisfaction Problem
A Graph-based Optimization Problem: Travelling Salesman Problem

A SAT Problem: Constraint Satisfaction Problem

This exemplary implementation can be found in the CSP_example.ipynb Jupyter notebook. Here, the solution to a Kakuro riddle with a 2x2 grid can be solved for arbitrary sums s0 to s3:

MQT ProblemSolver will return valid values to a, b, c, and d if a solution exists.

A Graph-based Optimization Problem: Travelling Salesman Problem

This exemplary implementation can be found in the TSP_example.ipynb Jupyter notebook. Here, the solution to a Travelling Salesman Problem with 4 cities can be solved for arbitrary distances dist_1_2 to dist_3_4between the cities.

MQT ProblemSolver will return the shortest path visiting all cities as a list.

A Hybrid Classical Quantum Computing Approach to the Satellite Mission Planning Problem

Additional to the two case studies, we provide a more complex example for the satellite mission planning problem. The goal is to maximize the accumulated values of all images taken by the satellite while it is often not possible to take all images since the satellite must rotate and adjust its optics.

In the following example, there are five to-be-captured locations which their assigned value.

Reducing the Compilation Time of Quantum Circuits Using Pre-Compilation on the Gate Level

Every quantum computing application must be encoded into a quantum circuit and then compiled for a specific device. This lengthy compilation process is a key bottleneck and intensifies for recurring problems---each of which requires a new compilation run thus far.

Pre-compilation is a promising approach to overcome this bottleneck. Beginning with a problem class and suitable quantum algorithm, a predictive encoding scheme is applied to encode a representative problem instance into a general-purpose quantum circuit for that problem class. Once the real problem instance is known, the previously constructed circuit only needs to be adjusted—with (nearly) no compilation necessary:

Following this approach, we provide a pre-compilation module that can be used to precompile QAOA circuits for the MaxCut problem.

Utilizing Resource Estimation for the Development of Quantum Computing Applications

Resource estimation is a promising alternative to actually execute quantum circuits on real quantum hardware which is currently restricted by the number of qubits and the error rates. By estimating the resources needed for a quantum circuit, the development of quantum computing applications can be accelerated without the need to wait for the availability of large-enough quantum hardware.

In resource_estimation/RE_experiments.py, we evaluate the resources to calculate the ground state energy of a Hamiltonian to chemical accuracy of 1 mHartree using the qubitization quantum simulation algorithm. The Hamiltonian describes the 64 electron and 56 orbital active space of one of the stable intermediates in the ruthenium-catalyzed carbon fixation cycle

In this evaluation, we investigate

different qubit technologies,
the impact of the maximal number of T factories,
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).

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:

(venv) $ pip install mqt.problemsolver

References

In case you are using MQT ProblemSolver in your work, we would be thankful if you referred to it by citing the following publication:

@INPROCEEDINGS{quetschlich2023mqtproblemsolver,
    title           = {{Towards an Automated Framework for Realizing Quantum Computing Solutions}},
    author          = {N. Quetschlich and L. Burgholzer and R. Wille},
    eprint          = {2210.14928},
    archivePrefix   = {arXiv},
    year            = {2023},
    booktitle       = {International Symposium on Multiple-Valued Logic (ISMVL)},
}