Zarankiewicz numbers z(m,n;3,4): SAT witnesses and DRAT-certified exact values (OEIS A006615 and A006625)
收藏资源简介:
Witness matrices and machine-checked certificates for Zarankiewicz numbers z(m,n;3,4) in the oriented convention (forbidden: 3-row × 4-column all-ones submatrices), supporting OEIS A006615 (a(n) = z(n,n;3,4)+1) and A006625 (a(n) = z(n,n+2;3,4)+1). This is Zarankiewicz's problem (1951); Erdős problem #713 supplies related asymptotic bipartite Turán context. Version 1 incorrectly cited #712, which concerns a different hypergraph Turán problem. Certified exact values (v3): z(12,12;3,4) = 90 (A006615 a(12) = 91, a new term), z(11,13;3,4) = 89 (A006625 a(11) = 90, a new term), and z(12,14;3,4) = 102 (A006625 a(12) = 103, a new term in v3). Certification partitions on the first row's one-count under double-lex symmetry breaking: every case is refuted by kissat, every retained proof is verified by drat-trim, and the exhaustiveness of each split is itself DRAT-certified. The package includes the full certificate structure, proof hashes, append-only evidence and independent witness-verification tools. Additional lower-bound witnesses: matrices for z(n,n;3,4), n = 13..21, and for z(13,15;3,4). The 12-by-14 k = 102 witness is part of a certified exact value, not only a lower bound. All 13 packaged witnesses were re-verified during the v3 build. Related work: Jeremy Tan, arXiv:2203.02283, introduced SAT and symmetry-breaking methods for square forbidden minors. Alexander Towell, DOI 10.5281/zenodo.19985042, published SAT partition decompositions for other z(m,n;3,4) values. The present exact terms, lex-prefix formulation and mechanically certified nested case covers are distinct contributions. Search, encodings and the certification pipeline were developed in close collaboration with an AI assistant (Claude, Anthropic). The supplied square witnesses through n = 16 were independently checked by Alex Towell (private communication, 2026-08-03): witnesses only, not the proof pipeline. This does not cover the 12-by-14 or 13-by-15 witnesses; he declines joint credit.



