Project: Optimal Circuit Synthesis with SAT · Searching Small Circuits
Lesson 1
For a fixed number of inputs, a Boolean function is just a bit string. This suggests a direct search for a smallest circuit computing the function. Start with the truth tables of the input variables. Then, at every step, choose two already available tables and one of the sixteen binary operations, apply the operation row by row, and add the resulting table.
If we keep the entire set of tables available after each step, this breadth-first search explores circuits in nondecreasing order of size. Hence, it not only gives the upper bound by finding a circuit computing a given function; at the same time it proves the lower bound on the size of any circuit computing it!
Problem. How many two-variable Boolean functions have minimum circuit size exactly one?