# Phase Oracle in Qiskit Solving Satisfiability Problems using Grover's Algorithm Section

In Qiksit Textbook, there is a section on solving satisfiability problems using Grover's Algorithm. For the 3SAT instance they construct the following phase oracle:

Is there any reasoning behind this construction? Are they using the solutions to the actual problem while constructing it?

For small boolean functions, up to 16 variables, tweedledum (the library used by Qiskit, repo|docs) synthesizes the circuit using the truth table: it uses to truth table to extract a special case of an ESOP (Exclusive-or Sum-Of-Products) representation, known as Pseudo-Kronecker expression. Indeed, if you are using this method to implement an oracle that will be use in Grover's algorithm to solve satisfiability, then you have the solution before using Grover's.

When dealing with bigger functions, however, this method will not work. Truth tables are expensive to represent, hence we need to represent bigger boolean functions through other means. In tweedledum, that method is Xor-And graph (XAG).

Once we build a XAG representation of a given function, tweedledum has a few options to how synthesize a reversible (quantum) circuit for it. This figures show a bird's eye view of two ways it can be done:

In one flow (upper path) the XAG is processed with a technique that synthesizes a reversible circuit for it, directly from the XAG. On the other flow, the big function is broken into smaller ones. A k-LUT graph is basically a graph of truth tables. $$k$$ is the number of inputs. Then the truth table based technique can be applied to each of these smaller functions, and combine them together to create the desired circuit.

Or look at tweedledum source code. You will find these techniques and others in the synthesis folder.

• Thank you very much for the detailed answer. Dec 6 '21 at 21:00

The process of turning a logical formula into a circuit is called synthesis, an active research field at the moment. Qiskit uses a library called tweedledum (repo|docs) for synthesising oracles into circuits.

This particular formula is in ESOP (Exclusive-or Sum-Of-Products) form. Checkout Evaluating ESOP Optimization Methods in Quantum Compilation Flows, by Meuli et al. The second author is the main developer of tweedledum, Bruno Schmitt.

• Thank you for the answer. I checked the paper and also the code but I could not understand how the exact circuit is created. My main question is whether do we need to know the truth table for the given formula to perform this synthesis. If we need to construct the truth table first, then this does not have use in practice when one tries to solve the 3-SAT problem, as this will require the pre-knowledge of the truth table and hence the satisfying assignment. Dec 6 '21 at 12:28
• Bruno, the tweedledum author, just answered with really good insights quantumcomputing.stackexchange.com/a/22205/1859 Dec 6 '21 at 16:43