Lesson 4

Test candidate sizes in increasing order. If \(F_{f,s}\) is satisfiable, read the selected predecessors and operation bits from the model to obtain a circuit. If it is unsatisfiable, no circuit of size \(s\) exists. Thus, the first satisfiable size is optimal, and the preceding UNSAT result is a machine-checkable lower-bound certificate.

In an implementation it is often faster to begin with any heuristic circuit of size \(U\) and test \(U-1,U-2,\dotsc\) until the first UNSAT result. Clauses learned while solving one size may also be reused in an incremental solver.