Research · Papers · Exact answers in open problems · MF-190
Exact B2 circuit size and machine-checkable certificate for 5-input MOD3,1
size_B2(MOD3,1 on 5 inputs) = 9
Published 2026-09-06
For everyone
Plain summary
This work establishes the exact minimum number of standard two-input logic gates needed to compute MOD3,1 on five binary inputs. The function outputs 1 when the sum of its five input bits leaves a remainder of 1 upon division by 3. Over the full two-input library B2—where NOT gates and signal branching are free—the minimal circuit requires exactly 9 gates.
Donald Knuth originally found this value using automated SAT search, but published no machine-checkable certificates. This work provides an explicit 9-gate circuit verified across all 32 five-bit input combinations, alongside a complete mathematical certificate proving that no 8-gate circuit exists. An independent proof checker verified the solver's certificate, removing the need to trust the search program itself.
Result
The exact circuit complexity of the 5-input MOD3,1 Boolean function over the full 2-input binary basis B2 is 9:
size_B2(MOD3,1 on 5 inputs) = 9
Specifically:
- A 9-gate normal chain over B2 computes MOD3,1 on 5 inputs.
- No circuit over B2 of size 8 or fewer computes MOD3,1 on 5 inputs.
Setting and definitions
Let x = (x1, x2, x3, x4, x5) ∈ {0,1}^5 be a 5-bit input vector with Hamming weight |x|. The modular counting function MOD3,r_n is defined by:
MOD3,r_n(x) = 1 iff |x| = r (mod 3)
For n = 5 and r = 1, the function returns 1 on inputs of weight 1 or 4, and 0 on inputs of weight 0, 2, 3, or 5.
The full binary basis B2 comprises all 16 Boolean functions from {0,1}^2 to {0,1}. Circuit size size_B2(f) is the minimum number of 2-input gates from B2 required to compute f; constants, NOT gates, and arbitrary output fanout carry zero cost.
Circuits are represented in Kojevnikov-Kulikov-Yaroslavtsev normal-chain form, where gates are ordered linearly and each computes a 2-input operation over primary inputs or outputs of earlier gates.
Method
The exact size size_B2(MOD3,1 on 5 inputs) = 9 combines an explicit upper-bound candidate at s = 9 with a certified unsatisfiability refutation at size s = 8.
Upper bound (s = 9)
An explicit 9-gate normal-chain circuit was evaluated over all 32 rows of {0,1}^5. The evaluation verified that the circuit matches the MOD3,1 truth table on every row, satisfying all constraints of the s = 9 SAT encoding. The candidate circuit is stored under identifier MOD3-01 in lanes/mod3-6-b2/BANK-CANDIDATES.md.
Lower bound (s = 8)
The non-existence of an 8-gate circuit was proved through certified propositional refutation:
- The synthesis problem for s = 8 was encoded into CNF using the Kojevnikov-Kulikov-Yaroslavtsev normal-chain formulation.
- Four symmetry-breaking constraints were added to prune isomorphic and suboptimal search branches. Each constraint carries a mathematical soundness proof ensuring at least one valid representative is preserved if an 8-gate circuit exists.
- kissat solved the resulting CNF to UNSAT in 110.6 seconds.
- kissat generated a 255 MB DRAT unsatisfiability certificate.
- drat-trim verified the DRAT certificate in 226 seconds, confirming the absence of satisfying assignments.
Verification receipts and run records are stored in VERIFY.md and the run box frontier/mod3/runs/.
Discussion
Knuth determined size_B2(MOD3,r_n) for n ≤ 5 by SAT search in The Art of Computer Programming (TAOCP Volume 4, Section 7.1.2, exercise 480), but did not provide machine-checkable lower-bound certificates.
The numerical value size_B2 = 9 originates with Knuth. This entry contributes the first complete, machine-checkable DRAT refutation that formally excludes size 8 circuits for 5-input MOD3,1.
Because the certificate was produced on the constrained CNF, the lower bound size_B2(MOD3,1 on 5 inputs) > 8 formally rests on the conjunction of the 255 MB DRAT refutation validated by drat-trim and the four soundness arguments for the symmetry-breaking constraints.
For everyone — the takeaway
What this means
Finding the smallest possible circuit for a logic function requires checking immense search spaces. Because search tools can harbor software bugs, automated proofs need an independent audit trail.
This result settles the exact two-input gate count for a 5-input remainder function. By combining an explicit 9-gate design with a machine-checked proof that 8 gates are impossible, it provides a certified benchmark for exact logic synthesis.
Attribution and prior art
Prior art: Knuth (TAOCP 7.1.2, exercise 480) determined the values for n ≤ 5 using SAT solving without publishing certificates. Sources: Knuth, TAOCP vol. 4A, section 7.1.2 · Kulikov, Pechenev, Slezkin 2022 (MFCS) · Kojevnikov, Kulikov, Yaroslavtsev 2009
Register references
- Entry: MF-190
- Knuth, D. E., *The Art of Computer Programming*, Volume 4, Section 7.1.2, exercise 480.
- Circuit candidate MOD3-01:
lanes/mod3-6-b2/BANK-CANDIDATES.md - Verification receipts:
VERIFY.md - Execution records: box
frontier/mod3/runs/
Every artifact named above is bundled in, or hashed by, this paper's evidence pack below.
Evidence pack
Everything needed to check this entry against its receipts: the register text, a manifest with a SHA-256 hash for every named receipt, and 2 of 2 receipt files bundled (16 KB). Anything not bundled is still hashed in the manifest and lives in the compute-box working trees.
Changelog
Last reviewed 2026-09-06
- 2026-09-06Published on this site.