Lesson 4

Test candidate sizes in increasing order. If \(F_{f,s}\) 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 practice, 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.