Project: Optimal Circuit Synthesis with SAT · Searching Small Circuits

Lesson 1

Nikolai Chukhin · Alexander S. Kulikov

For a fixed number of inputs, a truth table is just a bit string. This suggests a direct search. Start with the truth tables of the input variables. 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.

Breadth-first search explores circuits in nondecreasing order of size. The first state containing the target proves an upper bound by exhibiting a circuit and a lower bound because every smaller state has already been exhausted. States should be sets of available truth tables: the names and order of gates do not affect which continuations are possible.