SAT Circuits Synthesis Engine - Demonstration Notebook¶

The sat-circuits-engine open-source package provides capabilities of easily generating, executing and analyzing quantum circuits for satisfiability problems according to user-defined constraints.
The user-defined constraints for the satisfiability problem should obey a specific format (either a low-level format or a high-level format) which is explained in constraints_format.md.

The program is capable of generating Grover's operators, generating the overall SAT circuits, executing these circuits and exporting all data. It is built in a modular fashion such that a user can use some of these features or all of them.

A class named SATInterface allows access to more-or-less all the program's functionality, and it is recommended to access the features via this interface. It is possible to use SATInterface as an API (recommended), or to launch an interactive user interface with it (restrictive but intuitive).

Many ready-to-use examples may be found in test_data.json.

In this notebook you'll find the following sections:

  • API - Instructions and demonstrations for SATInterface's API.
  • Interactive user interface - Instructions for SATInterface's interactive interface.
  • Appendix A - A performance comparison to other synthesis engines for a specific benchmark satisfiability problem.
  • Appendix B - A pre-executed usage demonstration for the interactive user interface (see the Interactive user interface section first).

API¶

Demo 1 - Full Utilization of the API¶

In this example (example_13 from test_data.json) the constraints are defined in a high-level fashion, while exploiting pretty much all features:

  1. Generation of the suitable Grover's operator.
  2. Generation of the overall SAT circuit that solves the problem.
  3. Execution of the overall SAT circuit.
  4. Analysis of the execution's results.
  5. Representation and data-exportation of all the above.

The exported data includes circuit diagrams, QPY serialization files for all circuit objects, QASM 2.0 export file of the transpiled operator version, results data and metadata files. It is recommended to examine the exported data after exporting it in the following cells. The exported data path will be provided by the program before exportation (the program creates a unique data directory in sat_circuits_engine/data/generated_data/).

In addition, comments with annotations are integrated along this example's code.

In [5]:
# (1) Run this cell for obtaining the suitable Grover's operator for the defined satisfiability problem

from sat_circuits_engine import SATInterface
    
# Defining constraints and varibales in a high-level fashion
high_level_constraints_string = (
    "(x0 != x1)," \
    "(x3 != x4)," \
    "(x1 != x3)," \
    "(x3 != x5)," \
    "(x5 != x6)," \
    "(x0 != x2)," \
    "(x1 != x6)," \
    "(x4 != x6)"
)
high_level_vars = {"x0": 1, "x1": 1, "x2": 1, "x3": 2, "x4": 1, "x5": 1, "x6": 1}

# Initialization of the interface, `save_data=True` for exporting data into a dedicated directory
demo_1 = SATInterface(
    high_level_constraints_string=high_level_constraints_string,
    high_level_vars=high_level_vars,
    name="demo_1",
    save_data=True
)

# `obtain_grover_operator()` returns a dictionary of the form: `{
#     'operator': QC_OBJ,
#     'decomposed_operator': QC_OBJ,
#     'transpiled_operator': QC_OBJ,
#     'high_level_to_bit_indexes_map': MAP_OBJ
# }`.
# Transpilation is done according to the `transpile_kwargs` arg, which by default is set to:
# {'basis_gates': ['u', 'cx'], 'optimization_level': 3}.
grover_operator_data = demo_1.obtain_grover_operator(
    transpile_kwargs={'basis_gates': ['u', 'cx'], 'optimization_level': 3}
)

demo_1.save_display_grover_operator(grover_operator_data, display=True)

Data will be saved into 'sat_circuits_engine/data/generated_data/D10.03.23_T12.24.45_demo_1/'.

The system synthesizes and transpiles a Grover's operator for the given constraints. Please wait..
Done.

The operator diagram - high level blocks:

The operator diagram - decomposed:

The transpiled operator diagram saved into 'sat_circuits_engine/data/generated_data/D10.03.23_T12.24.45_demo_1/grover_operator/'.
It's not presented here due to its complexity.
Please note that barriers appear in the high-level diagrams above only for convenient
visual separation between constraints.
Before transpilation all barriers are removed to avoid redundant inefficiencies.

The transpilation kwargs are: {'basis_gates': ['u', 'cx'], 'optimization_level': 3}.
Transpiled operator depth: 124.
Transpiled operator gates count: OrderedDict([('cx', 118), ('u', 102)]).
Total number of qubits: 20.

The high-level variables mapping to bit-indexes:
{'x0': [0], 'x1': [1], 'x2': [2], 'x3': [4, 3], 'x4': [5], 'x5': [6], 'x6': [7]}

Saved into 'sat_circuits_engine/data/generated_data/D10.03.23_T12.24.45_demo_1/grover_operator/':
   Circuit diagrams for all levels.
   QPY serialization exports for all levels.
   QASM 2.0 export only for the transpiled level.
In [6]:
# (2) Run this cell for obtaining the overall SAT circuit:
# A `QuantumCircuit` object that solves the satisfiability problem, ready for execution on a backend.

from qiskit_aer import AerSimulator

# The number of iterations over Grover's iterator (= operator + diffuser) depends on the number of solutions.
# If the number of solutions is known, it is best to provide it.
# If the number of solutions is unknown, `solutions_num=-1` will initiate an classical
# iterative stochastic process that looks for an adequate number of iterations for the problem.
# Needless to mention, this process add some computational overheads.
# `solutions_num=-2` will generate a dynamic circuit to overcome the need for providing the number of solutions.
# NOTE - this is a BETA feature which is currently under development. For now it failes 
# to scale and works properly only for small circuits (~ < 15 qubits).
overall_circuit_data = demo_1.obtain_overall_sat_circuit(
    grover_operator=grover_operator_data['operator'],
    solutions_num=6,
    backend=AerSimulator()
)

demo_1.save_display_overall_circuit(overall_circuit_data, display=True)

The system builds the overall circuit..

For 6 solutions, 5 iterations needed.

The high level circuit contains 5 iterations of the following form:

The transpilation kwargs are: {'basis_gates': ['u', 'cx'], 'optimization_level': 3}.
Transpiled overall-circuit depth: 1062.
Transpiled overall-circuit gates count: OrderedDict([('u', 830), ('cx', 790), ('barrier', 45), ('measure', 8)]).
Total number of qubits: 20.

Exporting the full overall SAT circuit object..

Saved into 'sat_circuits_engine/data/generated_data/D10.03.23_T12.24.45_demo_1/overall_circuit/':
   A concised (1 iteration) circuit diagram of the high-level overall SAT circuit.
   QPY serialization export for the full overall SAT circuit object.
   QASM 2.0 export for the transpiled full overall SAT circuit object.
In [7]:
# (3) Run this cell for executing the overall SAT circuit and obtaining the results.

results_data = demo_1.run_overall_sat_circuit(
    circuit=overall_circuit_data['circuit'],
    backend=AerSimulator(),
    shots=300
)

demo_1.save_display_results(results_data, display=True)

The system is running the circuit 300 times on aer_simulator, please wait..
This process might take a while.
Done.
Circuit simulation execution time = 8.5 seconds.

The results for 300 shots are:

All counts:
[('01111110', 60), ('10001001', 51), ('01110110', 48), ('10010001', 47), ('10011001', 46), ('01100110', 44), ('11000011', 1), ('10101011', 1), ('01001101', 1), ('10100111', 1)]

Distilled solutions (6 total):
{'01111110', '01110110', '10010001', '10011001', '01100110', '10001001'}

The high-level variables mapping to bit-indexes:
{'x0': [0], 'x1': [1], 'x2': [2], 'x3': [4, 3], 'x4': [5], 'x5': [6], 'x6': [7]}

High-level format solutions: 
Solution 1: x0 = 0, x1 = 1, x2 = 1, x3 = 3, x4 = 1, x5 = 1, x6 = 0
Solution 2: x0 = 0, x1 = 1, x2 = 1, x3 = 2, x4 = 1, x5 = 1, x6 = 0
Solution 3: x0 = 1, x1 = 0, x2 = 0, x3 = 2, x4 = 0, x5 = 0, x6 = 1
Solution 4: x0 = 1, x1 = 0, x2 = 0, x3 = 3, x4 = 0, x5 = 0, x6 = 1
Solution 5: x0 = 0, x1 = 1, x2 = 1, x3 = 0, x4 = 1, x5 = 1, x6 = 0
Solution 6: x0 = 1, x1 = 0, x2 = 0, x3 = 1, x4 = 0, x5 = 0, x6 = 1

Demo 2 - Obtaining Specific Objects via API¶

In this example (example_7 from test_data.json) the constraints are defined in a low-level fashion, with the single purpose of obtaining Grover's operator.

In [8]:
# (1) Run this cell to obtain Grover's operator for the defined constraints

from sat_circuits_engine import SATInterface

# Initialization of the interface, `save_data=False` = not saving and exporting data
demo_2 = SATInterface(
    constraints_string="([4][3][2] == [0]),([2] == [3]),([3] == [4]),([0] != [1]),([8][7] == [3][2])",
    num_input_qubits=9,
    name="demo_2",
    save_data=False
)


# Obtaining Grover's operator objects
grover_operator_data = demo_2.obtain_grover_operator(
    transpile_kwargs={'basis_gates': ['u', 'cx'], 'optimization_level': 3}
)
operator = grover_operator_data['operator']
decomposed_operator = grover_operator_data['decomposed_operator']
transpiled_operator = grover_operator_data['transpiled_operator']


# Displaying results
print("The high level operator circuit diagram:")
display(operator.draw('mpl', fold=-1))

print("The decomposed operator circuit diagram:")
display(decomposed_operator.draw('mpl', fold=-1))

print(f"Gates count in the transpiled operator: {transpiled_operator.count_ops()}")

The system synthesizes and transpiles a Grover's operator for the given constraints. Please wait..
Done.
The high level operator circuit diagram:

The decomposed operator circuit diagram:

Gates count in the transpiled operator: OrderedDict([('cx', 78), ('u', 74)])

Interactive user interface¶

To initiate an intuitive (but somewhat restrictive) interactive interface, just execute a bare call to the API: SATInterface(). Follow the instructions and enter the appropriate inputs.

The default settings for the interactive user interface are:

  1. name = "SAT".
  2. save_data = True.
  3. display = True.
  4. transpile_kwargs = {'basis_gates': ['u', 'cx'], 'optimization_level': 3}.

See Appendix B for a demonstration of using the interactive interface.

Many ready-to-use examples data may be found in test_data.json - you might find it useful when playing around with the interactive interface.

For trying different satisfiability problems configurations just restart the interface by re-running the next cell.

In [ ]:
# Run this cell to initiate an interactive user interface

from sat_circuits_engine import SATInterface

SATInterface()

Appendix A¶

This appendix provides a performance benchmark of the sat-circuits-engine open-source software compared to the synthesis engine offered by Classiq.

As explained here, the problem to follow (example_29 from test_data.json) has been solved by Classiq's synthesis engine, which generated a Grover operator with the following properties:

  • Width (number of qubits): 29.
  • Depth: 197.
  • $CNOT$ gates count: 190.

Run the following cells and see yourself that sat-circuits-engine synthesizes a Grover operator for the same problem with the following properties:

  • Width (number of qubits): 27.
  • Depth: 211.
  • $CNOT$ gates count: 194.

It is clear that at least for this benchmark problem, the two engines are comparable in performance. The engine offered by sat-circuits-engine provides slightly inferior performance in depth and $CNOT$ gates count, and slightly superior performance in the number of qubits (the set of width, depth and $CNOT$ gates count properties is used here as a measure for performance).

In [1]:
# (1) Run this cell for obtaining the suitable Grover's operator for the defined satisfiability problem

from sat_circuits_engine import SATInterface

# Defining constraints and varibales in a high-level fashion
high_level_constraints_string = (
    "(x0 != x1)," \
    "(x2 + 2 != x3)," \
    "(x3 != x4)," \
    "(x3 != x1)," \
    "(x5 != x6)," \
    "(x0 != x2)," \
    "(x1 != x5)," \
    "(x4 != x6)," \
    "(x3 == 2)," \
    "(x2 + x4 + x3 == 3)"
)
high_level_vars = {"x0": 1, "x1": 1, "x2": 1, "x3": 2, "x4": 1, "x5": 1, "x6": 1}

# Initialization of the interface, `save_data=True` for exporting data into a dedicated directory
benchmark_demo = SATInterface(
    high_level_constraints_string=high_level_constraints_string,
    high_level_vars=high_level_vars,
    name="benchmark_demo",
    save_data=True
)

grover_operator_data = benchmark_demo.obtain_grover_operator(
    transpile_kwargs={'basis_gates': ['u', 'cx'], 'optimization_level': 3}
)

benchmark_demo.save_display_grover_operator(grover_operator_data, display=True)

Data will be saved into 'sat_circuits_engine/data/generated_data/D10.03.23_T13.19.39_benchmark_demo/'.

The system synthesizes and transpiles a Grover's operator for the given constraints. Please wait..
Done.

The operator diagram - high level blocks:

The operator diagram - decomposed:

The transpiled operator diagram saved into 'sat_circuits_engine/data/generated_data/D10.03.23_T13.19.39_benchmark_demo/grover_operator/'.
It's not presented here due to its complexity.
Please note that barriers appear in the high-level diagrams above only for convenient
visual separation between constraints.
Before transpilation all barriers are removed to avoid redundant inefficiencies.

The transpilation kwargs are: {'basis_gates': ['u', 'cx'], 'optimization_level': 3}.
Transpiled operator depth: 211.
Transpiled operator gates count: OrderedDict([('u', 208), ('cx', 194)]).
Total number of qubits: 27.

The high-level variables mapping to bit-indexes:
{'x0': [0], 'x1': [1], 'x2': [2], 'x3': [4, 3], 'x4': [5], 'x5': [6], 'x6': [7]}

Saved into 'sat_circuits_engine/data/generated_data/D10.03.23_T13.19.39_benchmark_demo/grover_operator/':
   Circuit diagrams for all levels.
   QPY serialization exports for all levels.
   QASM 2.0 export only for the transpiled level.
In [2]:
# (2) Run this cell for obtaining the overall SAT circuit:
# a `QuantumCircuit` object that solves the satisfiability problem, ready for execution on a backend.

from qiskit_aer import AerSimulator

overall_circuit_data = benchmark_demo.obtain_overall_sat_circuit(
    grover_operator=grover_operator_data['operator'],
    solutions_num=1,
    backend=AerSimulator()
)

benchmark_demo.save_display_overall_circuit(overall_circuit_data, display=True)

The system builds the overall circuit..

For 1 solutions, 12 iterations needed.

The high level circuit contains 12 iterations of the following form:

The transpilation kwargs are: {'basis_gates': ['u', 'cx'], 'optimization_level': 3}.
Transpiled overall-circuit depth: 3734.
Transpiled overall-circuit gates count: OrderedDict([('u', 3287), ('cx', 2784), ('barrier', 132), ('measure', 8)]).
Total number of qubits: 27.

Exporting the full overall SAT circuit object..

Saved into 'sat_circuits_engine/data/generated_data/D10.03.23_T13.19.39_benchmark_demo/overall_circuit/':
   A concised (1 iteration) circuit diagram of the high-level overall SAT circuit.
   QPY serialization export for the full overall SAT circuit object.
   QASM 2.0 export for the transpiled full overall SAT circuit object.
In [3]:
# (3) Run this cell for executing the overall SAT circuit and obtaining the results.
# WARNING: this specific circuit is heavy for a classical computer to simualte, it might take a while.

results_data = benchmark_demo.run_overall_sat_circuit(
    circuit=overall_circuit_data['circuit'],
    backend=AerSimulator(),
    shots=50
)

benchmark_demo.save_display_results(results_data, display=True)

The system is running the circuit 50 times on aer_simulator, please wait..
This process might take a while.
Done.
Circuit simulation execution time = 2108.04 seconds.

The results for 50 shots are:

All counts:
[('10010110', 50)]

Distilled solutions (1 total):
{'10010110'}

The high-level variables mapping to bit-indexes:
{'x0': [0], 'x1': [1], 'x2': [2], 'x3': [4, 3], 'x4': [5], 'x5': [6], 'x6': [7]}

High-level format solutions: 
Solution 1: x0 = 0, x1 = 1, x2 = 1, x3 = 2, x4 = 0, x5 = 0, x6 = 1

Appendix B¶

A demonstration of running the interactive user interface with example_17 from test_data.json in a high-level fashion:

In [13]:
from sat_circuits_engine import SATInterface

SATInterface()

Data will be saved into 'sat_circuits_engine/data/generated_data/D10.03.23_T13.02.21_SAT/'.

For a low-level setting of constraints, enter '0'.For a high level setting, enter '1': 1

Enter a high-level constraints string: (x2 == x1),(x0 == 6)

Enter a dictionary of variables setting in a Python syntax, while keys are variables-names and values are bits-lengths (Dict[var, num_bits]): {"x0": 3, "x1": 1, "x2": 1}

The system synthesizes and transpiles a Grover's operator for the given constraints. Please wait..
Done.

The operator diagram - high level blocks:

The operator diagram - decomposed:

The transpiled operator diagram saved into 'sat_circuits_engine/data/generated_data/D10.03.23_T13.02.21_SAT/grover_operator/'.
It's not presented here due to its complexity.
Please note that barriers appear in the high-level diagrams above only for convenient
visual separation between constraints.
Before transpilation all barriers are removed to avoid redundant inefficiencies.

The transpilation kwargs are: {'basis_gates': ['u', 'cx'], 'optimization_level': 3}.
Transpiled operator depth: 36.
Transpiled operator gates count: OrderedDict([('u', 27), ('cx', 22)]).
Total number of qubits: 8.

The high-level variables mapping to bit-indexes:
{'x0': [2, 1, 0], 'x1': [3], 'x2': [4]}

Saved into 'sat_circuits_engine/data/generated_data/D10.03.23_T13.02.21_SAT/grover_operator/':
   Circuit diagrams for all levels.
   QPY serialization exports for all levels.
   QASM 2.0 export only for the transpiled level.

To stop here, enter '0'. For obtaining also the overall circuit, enter '1': 1

If the expected amount of solutions is known, please enter it (it is the easiest and optimal case).

If the expected amount of solutions is unknown, please enter the value '-1'.
In this case the program will look for an adequate (optimal or near optimal)
number of iterations for the given SAT problem, using an iterative stochastic process.
This process might cause significant overheads and might take some time.
Another option is using a dynamic circuit layout (this feature is in BETA version,
and suffers from bugs and poor scaling) - for this option enter the value '-2'.
Please enter the expected number of solutions ('-1' or '-2' for unknown): -1

For running the circuit on local `aer_simulator`, enter '0'.
For running the circuit on `ibmq_qasm_simulator` via cloud, enter '1'.
NOTE: A saved IBMQ API token need to be available on your machine for option '1'.
For other custom backends please use the API and not this interactive interface.
Your input: 0

Obtaining aer_simulator..

Please wait while the system checks various solutions..

Checking iterations for precision = 10:
    Checking iterations = 1
    Checking iterations = 2
    Checking iterations = 3
Found number of iterations in 0.77 seconds.

An adequate number of iterations found = 3.

The high level circuit contains 3 iterations of the following form:

The transpilation kwargs are: {'basis_gates': ['u', 'cx'], 'optimization_level': 3}.
Transpiled overall-circuit depth: 296.
Transpiled overall-circuit gates count: OrderedDict([('u', 228), ('cx', 174), ('barrier', 13), ('measure', 5)]).
Total number of qubits: 8.

Exporting the full overall SAT circuit object..

Saved into 'sat_circuits_engine/data/generated_data/D10.03.23_T13.02.21_SAT/overall_circuit/':
   A concised (1 iteration) circuit diagram of the high-level overall SAT circuit.
   QPY serialization export for the full overall SAT circuit object.
   QASM 2.0 export for the transpiled full overall SAT circuit object.

To stop here, enter '0'. For running the overall circuit and obtain data, enter '1': 1

Please enter the number of shots desired: 512

The system is running the circuit 512 times on aer_simulator, please wait..
This process might take a while.
Done.
Circuit simulation execution time = 0.36 seconds.

The results for 512 shots are:

All counts:
[('11110', 244), ('00110', 244), ('10000', 3), ('10001', 3), ('00101', 3), ('00100', 2), ('00000', 2), ('01101', 1), ('10011', 1), ('01100', 1), ('01010', 1), ('11001', 1), ('00011', 1), ('10100', 1), ('11000', 1), ('10101', 1), ('00001', 1), ('01000', 1)]

Distilled solutions (2 total):
{'11110', '00110'}

The high-level variables mapping to bit-indexes:
{'x0': [2, 1, 0], 'x1': [3], 'x2': [4]}

High-level format solutions: 
Solution 1: x0 = 6, x1 = 1, x2 = 1
Solution 2: x0 = 6, x1 = 0, x2 = 0


Done saving data into 'sat_circuits_engine/data/generated_data/D10.03.23_T13.02.21_SAT/'.
Out[13]:
<sat_circuits_engine.interface.interface.SATInterface at 0x7f559407dac0>