Exact majority-inverter complexity of small Hamming-weight counters: PAR_5 = 6, SUM_5 = 9, SUM_6 and SUM_7 in [9, 12]

We determine, or bound, the minimum number of gates of majority-inverter graphs (three-input majority gates, free inverters, a free constant, shared gates) for small Hamming-weight counters. The parity of five inputs needs 6 gates, and SUM_5, whose three outputs are the bits of the Hamming weight of five inputs, needs 9; for SUM_6 and SUM_7 the minimum lies between 9 and 12. Every lower bound rests on unsatisfiable formulas whose DRAT proofs were checked by drat-trim; those for SUM_6 and SUM_7 follow from SUM_5 by fixing an input to 0. Three short written arguments, proved in the text, connect the formulas to the circuit statements; one of them, the soundness of an input-symmetry break, is required in the main proof only for SUM_5 at 8 gates, and the floors for SUM_6 and SUM_7 inherit that use through Lemma R. An 8-gate run without the break, which would test that argument independently, has not finished; the value 9 does not depend on it. At five inputs, two full adders and a half adder are already optimal. We also report how the solver time grows from one gate count to the next and the techniques we measured that did not pay off.