Grover search: SAT problem

In this notebook I’m going to show how to use qlasskit for solving a SAT problem. A SAT problem, or Boolean satisfiability problem, asks whether a given Boolean formula can be satisfied by assigning true or false values to its variables.

We define our SAT problem writing an oracle function that receive a list of 5 boolean variables, and return the logical AND between all the elements (negating those whose index is even).

from qlasskit import qlassf, Qlist, Qint, Qint4


@qlassf
def sat(b_list: Qlist[bool, 5]) -> bool:
    r = True
    i = 0
    for b in b_list:
        r = r and (b if i % 2 == 0 else not b)
        i += 1
    return r


sat.export("qiskit").draw("mpl")

Then we use Grover to search for input values leading to a True result from our SAT oracle:

from qlasskit.algorithms import Grover

q_algo = Grover(sat, True)
qc = q_algo.export("qiskit")

We use qiskit to run the simulation; as we expected from our simple problem, the solution is the list [True, False, True, False, True] where variable in even positions are negated.

from qiskit import QuantumCircuit, transpile
from qiskit.visualization import plot_histogram
from qiskit_aer import AerSimulator

qc.measure_all()
simulator = AerSimulator()
circ = transpile(qc, simulator)
result = simulator.run(circ).result()
counts = result.get_counts(circ)

counts_readable = q_algo.decode_counts(counts, discard_lower=15)
plot_histogram(counts_readable)