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.