The XAG and AIG gaps at five inputs: where the XAG gap reaches 2, and where parity stands

For a Boolean function f and a gate basis, opt(f) is the least number of gates of a circuit for f, tree(f) the least number of gates of a formula, and gap(f) = tree(f) − opt(f). This note collects what we have established about two questions at five inputs, and marks the status of each statement.

Line 1. Where does gap_XAG ≥ 2 live? If the published five-input tables are optimal (hypotheses H1 and H2 below), 6,828 of the 616,126 NPN classes have XAG gap at least 2, and all of them have 6 ≤ opt_XAG ≤ 10. Both edges of that window hold without their optimality assumptions, for whichever classes have gap_XAG at least 2. At the lower edge, a theorem proved in this note says that opt_XAG ≤ 5 forces gap_XAG ≤ 1, and an exhaustive enumeration of circuits, simulated formulas and an exhaustive dynamic program over formulas show that exactly five classes reach gap 2 at opt_XAG = 6 and that none reaches gap 3 below opt_XAG = 7. At the upper edge, every formula of the Lflib5 library, evaluated by our own parser, has at most 12 gates, so tree_XAG ≤ 12 in every class and gap_XAG ≥ 2 forces opt_XAG ≤ 10. Which classes have gap at least 2, and how many, rests on the tables. Almost none of the 6,828 come from composing smaller functions on disjoint variables: 3 have a simple disjoint decomposition in Paul's sense [Paul 1976], f = F(g(x_S), x_T) with S and T disjoint; none of them is two functions of disjoint variables joined by one gate; and those three have (opt_XAG, tree_XAG) = (7, 9), which we can establish without the tables, for one of the three only through a substitution law proved in the appendix, a proof read by its author and by language models; the half of that law used here, the one about formulas, is also formalised in Lean.

Line 2. Does parity stop being extremal for the AIG gap? Parity has AIG gap 15 at five inputs, if the published five-input table of formula sizes of Cox and Healy is right (hypothesis H3 below); its circuit size is a theorem of the literature. The class 0x1669e996, one of the three classes of largest formula size in that table, has gap 15 as well if Lemma S and H3 hold, Lemma S being a lemma proved in the appendix, whose proof has been read by its author and by language models and is also formalised in Lean; so if both hold, this class ties with parity and does not beat it. Of the other two classes of largest formula size, 0x16696997 cannot beat parity if a sketched gate-elimination step is correct and H3 holds, and 0x16686997 is open. Whether any five-input function has AIG gap 16 or more is open.