Project: Optimal Circuit Synthesis with SAT · Exact Circuit Synthesis
Lesson 1
A truth table specifies what a Boolean function does, but not how to compute it. The exact synthesis problem asks for a smallest circuit computing a given truth table. Throughout the project, every gate has fan-in two, but its operation may be any Boolean function of its two inputs.
We describe such an operation by four bits \[b_{00}b_{01}b_{10}b_{11}.\]
The bit \(b_{uv}\) is the output when the first input is \(u\) and the second is \(v\). Thus, \(\texttt{0001}\), \(\texttt{0111}\), and \(\texttt{0110}\) describe AND, OR, and XOR, respectively.
Inputs and earlier gates may be reused without cost. This sharing is what distinguishes circuits from formulas and makes exact synthesis interesting.
Problem. Write the four-bit operation string for implication \(x\to y\).