An exact-synthesis audit of the Simplifier AIG database: a quantified complement to its stated optimality gap

The Simplifier tool of Averkov et al. replaces small subcircuits by circuits taken from a precomputed database of AND-inverter graphs (AIGs) for Boolean functions with three inputs and up to three outputs. Its authors state that the AIG part of the database could not be proven optimal throughout. We ran an exhaustive exact-synthesis pass over the database at a fixed snapshot and report two things, which we keep apart. First, on the entries the tool can look up, the audit agrees with the paper and quantifies its gap: under the class partition the paper uses, every one of the 7,433 reachable classes is decided. All 7,205 stored with at most 9 ANDs are confirmed minimum by a SAT solver; of the 222 stored with 10 ANDs, 221 are confirmed and one is lowered to 9; of the 6 stored with 11 ANDs, five are confirmed and one is lowered to 10. The 203 classes, and the minimum of one more, that our 30-second cap had left open were closed by rerunning one line of each at a cap of seven days, and drat-trim verified a proof of unsatisfiability for the CNF of each of the 204 deciding calls. Under our reading of the paper's Figure 4, its presumably optimal circuit lies in one of the five confirmed classes. The improvements on reachable entries fall in the two lowered classes, both in rows the paper itself marks as upper bounds. The AIG database shipped with Cirbo, a tool by several of the same authors, stores the same six classes at 11 ANDs and, in the classes both files share, no circuit below our minimum; outside classes with a literal output, it departs from our minimum only in the same two classes. Second, 10,390 further entries admit a smaller circuit, but every one of them has an output equal to an input literal or two complementary outputs, and the tool's lookup discards such outputs before it searches; these improvements are a property of the file, not of what the tool does. We also find one orbit of six lookup keys that the database lacks, and on a sample of 2,000 entries we measure the trade-off between size and depth. Apart from those 204 calls, the optimality verdicts are solver output without proof certificates; the improved circuits are independently checkable. We dispute no statement of the paper.