Skip to content

Demo: Solving 3-SAT Using Grover's Algorithm

Introduction

Grover's algorithm [1,2] is a quantum search algorithm that enables searching a dataset of \(N\) items using \(O(\sqrt{N})\) queries, in contrast to classical algorithms which require \(\Omega(N)\) queries in the worst case. Using the algorithm allows us to speed-up various computations that are considered classically intractable. For example, the 3-SAT problem [3] is a famous \(\text{NP-Complete}\) problem, a solution of which allows solving any problem in the complexity class \(\text{NP}\).

In this demo, we will show how the Classiq platform enables us to solve an instance of 3-SAT using Grover's algorithm at a higher functional level, avoiding the implementation details one is usually exposed to when using other platforms.

The 3-SAT Formula

We now specify the 3-CNF [4] formula that we wish to find a solution for: $$ (x_1 \lor x_2 \lor x_3) \land (\neg x_1 \lor x_2 \lor x_3) \land (\neg x_1 \lor \neg x_2 \lor \neg x_3) \land (\neg x_1 \lor \neg x_2 \lor x_3) \land (x_1 \lor x_2 \lor \neg x_3) \land (\neg x_1 \lor x_2 \lor \neg x_3) $$

formula = """
    ( ( x1) or ( x2) or ( x3) ) and
    ( (not x1) or ( x2) or ( x3) ) and
    ( (not x1) or (not x2) or (not x3) ) and
    ( (not x1) or (not x2) or ( x3) ) and
    ( ( x1) or ( x2) or (not x3) ) and
    ( (not x1) or ( x2) or (not x3) )
"""

Using the package truth-table-generator [5], we can see the formula above has 4 solutions (out of 8 possible assignments):

%%capture
!pip install -q truth-table-generator==1.1.2
try:
    import ttg

    print(ttg.Truths(["x1", "x2", "x3"], [formula[1:-1]]))
except:
    print("Please import 'truth-table-generator' in order to print the truth table")
+------+------+------+------------------------------------------------+
|  x1  |  x2  |  x3  |          ( ( x1) or ( x2) or ( x3) ) and       |
|      |      |      |         ( (not x1) or ( x2) or ( x3) ) and     |
|      |      |      |      ( (not x1) or (not x2) or (not x3) ) and  |
|      |      |      |       ( (not x1) or (not x2) or ( x3) ) and    |
|      |      |      |         ( ( x1) or ( x2) or (not x3) ) and     |
|      |      |      |         ( (not x1) or ( x2) or (not x3) )      |
|------+------+------+------------------------------------------------|
|  1   |  1   |  1   |                       0                        |
|  1   |  1   |  0   |                       0                        |
|  1   |  0   |  1   |                       0                        |
|  1   |  0   |  0   |                       0                        |
|  0   |  1   |  1   |                       1                        |
|  0   |  1   |  0   |                       1                        |
|  0   |  0   |  1   |                       0                        |
|  0   |  0   |  0   |                       0                        |
+------+------+------+------------------------------------------------+

Note that since there are multiple satisfying assignments for the formula, the goal of the Grover quantum algorithm is to find one of them. This is contrast to the usual description of the search problem (found in 2), in which there is a single solution (out of \(N\) possibilities).

Loading the Grover search model

Next, we load the Grover search model which we use to find the solution. To specify the model, we need to define the oracle it uses. Each oracle call is analogous to a classical query. In this case, we define an oracle based on the 3-CNF formula defined earlier. Along with the standard definitions of the arithmetic expression for the oracle and the variable definitions, the oracle also requires us to specify the uncomputation method (in this case - "optimized"). In addition, we define the number of grover operator repetitions in the model (which is based on the frequency of solutions in the search space), and the number of samples to take on this circuit.

from classiq import RegisterUserInput, construct_grover_model

register_size = RegisterUserInput(size=1)

qmod = construct_grover_model(
    num_reps=1,
    expression="(" + formula + ")",
    definitions=[
        ("x1", register_size),
        ("x2", register_size),
        ("x3", register_size),
    ],
)
from classiq import write_qmod

write_qmod(qmod, "3_sat_grover")

Synthesizing the Circuit

We proceed by synthesizing the circuit using Classiq's synthesis engine. The synthesis should take approximately several seconds:

from classiq import QuantumProgram, synthesize

qprog = synthesize(qmod)

Showing the Resulting Circuit

After Classiq's synthesis engine has finished the job, we can show the resulting circuit in the interactive GUI:

circuit = QuantumProgram.from_qprog(qprog)
circuit.show()
Opening: https://platform.classiq.io/circuit/6b9562a5-c126-4489-8463-3fa4b21ef13a?version=0.41.0.dev39%2B79c8fd0855
print(circuit.transpiled_circuit.depth)
429

Executing the circuit

Lastly, we can execute the resulting circuit with Classiq's execute interface, using the execute function.

from classiq import execute, set_quantum_program_execution_preferences
from classiq.execution import (
    ClassiqBackendPreferences,
    ClassiqSimulatorBackendNames,
    ExecutionPreferences,
)

backend_preferences = ExecutionPreferences(
    backend_preferences=ClassiqBackendPreferences(
        backend_name=ClassiqSimulatorBackendNames.SIMULATOR
    )
)

qprog = set_quantum_program_execution_preferences(qprog, backend_preferences)
optimization_result = execute(qprog).result()
res = optimization_result[0].value

Printing out the result, we see that our execution of Grover's algorithm successfully found the satisfying assignments for the input formula:

res.counts_of_multiple_outputs(("x1", "x2", "x3"))
{('0', '1', '1'): 478, ('0', '1', '0'): 522}

References

[1]: Grover, Lov K. "Quantum mechanics helps in searching for a needle in a haystack." Physical review letters 79.2 (1997): 325.

[2]: Grover's algorithm (Wikipedia)

[3]: 3-SAT Problem (Wikipedia)

[4]: Conjunctive Normal Form (Wikipedia)

[5]: truth-table-generator (PyPI)