Project: Optimal Circuit Synthesis with SAT · Seven-Segment Display
Lesson 3
A straightforward construction computes an indicator for each decimal digit and ORs the required indicators for every segment. A SAT solver can often do better by discovering intermediate functions shared in less obvious ways.
The same method applies to instruction decoders, cryptographic S-boxes, arithmetic blocks, and error-correcting-code logic. One can also optimize depth instead of gate count, restrict the gate library to match a fabrication technology, or synthesize several outputs under a joint area bound. In every case the pattern is the same: encode candidate implementations, ask SAT for a construction, and use UNSAT to certify a lower bound.
For the curious 🤓
The first attempt to optimize every function of four variables was published by Howard Aiken's staff at the Harvard Computation Laboratory in 1951. They worked by hand, using heuristic methods to construct tables of the best circuits they could find, but without proving optimality of the found circuits. Their circuits modeled vacuum tubes, so their cost \(V(f)\) was quite different from our number of gates. They allowed NOR, OR, and NAND gates with \(k\) inputs at cost \(k\). An input to a gate could be a variable, a complemented variable, or the output of an earlier gate. At the top level they could take an AND of any number of gate outputs for free.
Their model is even not symmetric under complement. For example, \(x\land y=\operatorname{NOR}(\bar x,\bar y)\) has cost \(2\), and \(\bar x\lor(\bar y\land\bar z)=\operatorname{NAND}(x,\operatorname{OR}(y,z))\) has cost \(4\). But its complement \(x\land(y\lor z)=\operatorname{AND}(\operatorname{NOR}(\bar x),\operatorname{OR}(\bar y,\bar z))\) has cost \(3\), because the final AND was free. Consequently the Harvard group had to consider \(402\) essentially different classes of four-variable functions instead of the usual \(222\) classes.
The first computer program to find provably optimal circuits was written by Leo Hellerman in 1963. It found the minimum number of NOR gates for every function of three variables. In 1977, Frank M. Liang established the minimum circuit size for every function of four variables. Then, in 2008, Donald Knuth reported a complete computation for five variables functions. We used his ideas in this project. The number of functions of five variables is approximately \(4.2 \cdot 10^{9}\), whereas the number of functions of six variables is already \(1.8 \cdot 10^{18}\); hence, it is infeasible to find optimal circuits for all of them.