SAT Circuits Synthesis Engine

This Python-Qiskit-based package provides capabilities of easily generating, executing and analyzing quantum circuits for satisfiability problems according to user-defined constraints. The circuits being generated by the program are based on Grover's algorithm and its amplitude-amplification generalization.

The term SAT is used throughout the package's content as an abbreviation for "satisfiability", not as a term for "boolean satisfiability problems". This software is capable of generating quantum circuits for multiple types of satisfiability problems, not only for boolean satisfiability problems (known as k-SAT).

Motivation

Today's current quantum software stack is pretty thin. Quantum programming is being performed mostly at the level of qubits and logic gates. While for low amounts of qubits it might be sufficient, as technology advances and quantum processors scale up, it becomes infeasible to design quantum programs for increasing amounts of qubits. Some adequate layers of abstraction are needed to really exploit the power of future quantum computers.

Exploiting Grover's and the amplitude-amplification algorithms for satisfiability-problems solving offers a quadratic speed-up compared to the classical counterparts, assuming the problem has no unique structure (which is analogous to an unsorted database, in the simple database-search problem). A time complexity of $O(\sqrt{N})$ up to an oracle (i.e, $O(\sqrt{N})$ calls to Grover's operator, that is the oracle) is offered by the program, while $N$ is the dimension of the solutions space (analogous to the size of the database in a simple database-search problem). The classical solution offers a time complexity of $O(N)$.

Intention

This program aspires to provide a fully automatic quantum program synthesis solution for satisfiability problems. For now (version 3.1.1) - the program offers a decent layer of abstraction along with various features. Yet, there are still many more factors to optimize and still some desired features are missing. These issues will be taken care of in the next releases.

Grover's algorithm (much like all the other "pure" quantum algorithms - by "pure" I mean not classical-hybrid) is intractable for current NISQ devices, certainly at scale. Therefore the program relies solely on (noiseless) classical simulators and is aimed to use on a future fault-tolerant quantum computer.

Recent evolvements in the field of quantum control (see Fire Opal by Q-CTRL) now allow obtaining some useful results out of Grover's algorithm circuits, but still only for shallow and small circuits. I.e, one can use this program to synthesize circuits also for real quantum devices, but still at a small scale for now. The author has tried a 7-qubits, ~100 layers-depth circuit (example_1 from test_data.json) and managed to extract the correct solutions (the results are still quite noisy, but distinguishable) from a real quantum backend.

Requirements and Instructions

Installation:

1. git clone https://github.com/ohadlev77/sat-circuits-engine.git.
2. From the root directory of the package - run pip install ..
   a) All dependencies (requirements.txt) will be installed automatically.
   b) Now the package is available by running import sat_cirucits_engine from anywhere.
3. Supported Python versions are: 3.9, 3.10, 3.11.

For testing run python3 -m unittest from the root directory.

Usage

1. In demos.html and demos.ipynb there are detailed demonstrations explaining how to use this package. demos.html is a static HTML page with pre-executed demonstrations, while demos.ipynb is a dynamic Jupyter notebook with the same demonstrations ready to be executed by a user.
2. The program's features are accessible either from a terminal or a Jupyter notebook. The visualizations are nicer in a Jupyter notebook, though even when using a terminal the program provides a simple interface to export rich visualizations files (explained within the demos files).
3. In short (For full explanations see the demos files), all features are accessible via a class named SATInterface (from sat_circuits_engine import SATInterface). A bare call to an instance of this class (SATInterface()) will initiate an interactive user interface (an intuitive interface but also somewhat restrictive). For full flexibility one should use the API of SATInterface (recommended, but it is required to study the API, either via the docstrings of SATInterface, or by overviewing the demos, or both). Again, see demos.html or demos.ipynb for full annotations.
4. It is a must to understand the constraints input format used in this package in order to use the package. That is explained in detail in constraints_format.md.
5. Many ready-to-use examples may be found in test_data.json.

For Developers

1. Development requirements are in requirements-dev.txt (pip install -r requirements-dev.txt from the root directory).
2. Before pushing changes run tox from the root directory - tests in python 3.9-3.11, formatting, linting and coverage tests will be executed. Running a single specific tox configuration is also possible:

• tox -epy39 or tox -epy310 or tox -epy311 for the desired python version.
• tox -elint for linting check by pylint (minimum rate required is 9.0).
• tox -eblack for formatting check by black.
• tox -ecoverage for tests-coverage check by coverage (minimum 80% coverage is required).