Records of the DRAT checks for the minimum circuit size of four-input functions in AIG, MIG and XAG: captures, CNF and proof hashes, and scripts

Data and code behind Section 6 of Auditing published circuit tables against exact computation (concept doi:10.5281/zenodo.23642615, version 1.3 and later), which cites this record in Section 7. For the 222 NPN classes of four-input Boolean functions in each of three bases (AIG: two-input AND gates; MIG: three-input majority gates; XAG: two-input AND and XOR gates; inverters free, cost = number of gates), every lower bound of two or more gates rests on refutations checked by drat-trim, with no symmetry breaking between gates; a bound of one gate is read off the truth table, and the upper side is a circuit simulated on all 16 rows. This record holds the records of those checks, not the proofs, for 665 of the 666 pairs of class and basis; four-input parity in MIG is in an earlier record. Contents. One capture per class and basis, 665 in all (AIG 222, MIG 221, XAG 222), each with the SHA-256 and size of every CNF and every DRAT proof, the kissat and drat-trim results for every k below the minimum, the witness circuit at the minimum, and a negative control (the last proof checked against the satisfiable CNF at the minimum and rejected by drat-trim; skipped, and recorded as skipped, for the five classes whose proof exceeded 512 MiB); the summary table; the tables of minima the run was checked against; the driver, the three encoders and the drat-trim wrapper; a checker of the records that simulates the witnesses with its own code and does not rerun the solver or drat-trim; and the output of four checks run from this package when it was assembled, one of which regenerates all 3,651 CNFs and finds the recorded hashes. What is not included. The CNFs and the proofs. The CNFs regenerate from the encoders; the proofs (26.2 GB in AIG, 63.2 GB in MIG and 1.9 GB in XAG) were deleted after checking, and the drat-trim outputs and hashes are kept. Four-input parity in MIG has its refutations in the earlier record 10.5281/zenodo.23382607, whose pinned CNF hashes the encoder here reproduces. Limits. DRAT certifies the CNFs, not that they encode the intended question; that step rests on the encoders and is argued in the paper, not machine-checked. drat-trim is not formally verified. Text and data under CC BY 4.0; code under MIT.