Base laws for the formula–circuit gap at four inputs: AIG, MIG and XAG compared class by class

For a Boolean function f and a gate basis, let opt(f) be the minimum number of gates of a circuit for f and tree(f) the minimum number of gates of a formula (a circuit in which every gate feeds at most one gate), and call gap(f) = tree(f) − opt(f) the price of forbidding reuse. We compare this price in three bases with free inversion, AND-inverter graphs (AIG), majority-inverter graphs (MIG) and XOR-AND graphs (XAG), on each of the 222 NPN classes of four-input functions. The per-basis values are not new, though not all are published class by class: the size distributions in all three bases have been published before, per-class values only for some of the six columns, and we deposited the per-class values of all three bases earlier as a dataset; we also assume, without having checked, that the two XAG sizes of every class are already in Knuth's book.

What we report is how the three gaps relate on the same class. The maximum gap is 6 in AIG, 3 in MIG and 1 in XAG. Adding gates to the basis does not always lower the gap. Every AIG gate is also an MIG gate and an XAG gate; no class pays a gap in XAG without paying in AIG, but 11 classes pay a gap in MIG and in neither of the other two bases. MIG and XAG are not comparable gate for gate, and their gaps are not ordered either: 3 classes pay in XAG and not in MIG. Only one class pays in all three bases, the function E₂ that is true when exactly two of the four inputs are true.

We add two smaller results, each stated with its scope: in the optimal AIG cascade for parity the operand-cone intersection at the output gate has 3(n − 2) gates for n = 3 to 12, so its agreement with the gap at n = 3 and n = 4 does not continue; and over XAG at three inputs every essential variable can be read exactly once by some minimum formula, a fact that fails at four inputs.

Every number written in digits from the Abstract to Section 5 is checked by a script against the project's artefacts, and the paper lists, number by number, where each one comes from. The script checks finite data: where a statement is made for every n, it checks the instances it has, and the general case rests on a cited theorem or on algebra written out in the text. Statements without a number are checked only where the provenance table says so.