Quantum Computing Stack Exchange is a question and answer site for engineers, scientists, programmers, and computing professionals interested in quantum computing. It only takes a minute to sign up.
Sign up to join this community
In Qiskit 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.
You can read more about it in:
Or look at tweedledum source code. You will find these techniques and others in the synthesis folder.
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.
