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