Lesson 3

Exhaustive computation becomes much harder at four and five variables, where shared subexpressions can improve a circuit. Nevertheless, complete optimal-size tables are known. Donald Knuth computed optimal costs for all functions of five variables, building on earlier computations for three and four variables. Such tables are not merely collections of clever constructions: each claimed optimum also requires ruling out every smaller circuit.

SAT solvers give us a general way to perform both tasks.