Parity in majority-inverter graphs: enumerations, censuses, cell certificates and solver logs

Data and code behind the note Parity in majority-inverter graphs: exact values for n ≤ 5, an interval for n = 6, and a conjecture (doi:10.5281/zenodo.23902529), which cites this record as [D]. Model: majority-inverter graphs (MIGs) with 3-input majority gates, free inverters, a free constant and three distinct operands per gate; cost = number of majority gates. The note gives opt(PAR_n) = 0, 3, 3, 6, 6 for n = 1..5 and 6 ≤ opt(PAR_6) ≤ 9. Contents. The exhaustive enumerations for n = 2, 3 (192 labelled optimal circuits each, none with two gates); the evaluation of the circuits returned by the exact-synthesis tool percy for PAR_4 and PAR_5; the solver log of the 6-gate formula for PAR_6 (UNSAT without a proof), the decoded and simulated 9-gate circuit, and the record of the 7- and 8-gate runs stopped without a verdict; the drat-trim outputs of two cells of PAR_4 with a bound on full gates, one of them split into 80 parts, each with its own checked DRAT proof; the 80 + 160 branch files of the censuses of all labelled optimal circuits for n = 4 and n = 5; the optimal size of each of the 222 NPN classes of four-variable functions, with its comparison with the counts published by Soeken et al. (DATE 2016); the scripts that produced them; and the output of fourteen checks run from this package when it was assembled. What is not included. The DRAT records of PAR_4 and PAR_5 at sizes 1 to 5 are in the earlier record 10.5281/zenodo.23382607. Formulas and proofs are not stored: the formulas regenerate from the encoder, and their SHA-256 values are recorded in the logs, or, for the cell split into 80 parts, pinned in the script that rebuilds it; the proofs were deleted after checking because of their size, and the drat-trim outputs are kept. Third-party sources are not included. Limits. DRAT certifies the formulas, not that they encode the intended question; that step is written out in the note and is not machine-checked. The 6-gate result for PAR_6 has no proof, and the censuses and the percy runs are evidence, not proofs. Text and data under CC BY 4.0; code under MIT.