Complete uniform hypergraphs that support an unsatisfiable CNF: two open cells, one correction, and the threshold sequence
Abstract
Karve and Hirani attach to a hypergraph g the set of CNFs that live on it — one clause per edge, on exactly that edge's variables, with an arbitrary choice of signs — and call g totally satisfiable when every such CNF is satisfiable. For the complete a-uniform hypergraph Ka(a, b) on b vertices they publish a table of statuses for a,b ≤ 7, in which two cells are printed unknown. We settle both: Ka(4, 7) is not totally satisfiable, by an explicit 35-clause CNF that all 128 assignments falsify, and Ka(5, 7) is totally satisfiable, because C(7, 5)2²=84<128. We also correct a third cell: the table prints Ka(3, 5) as unsat in boldface, and Ka(3, 5) is in fact totally satisfiable — an exhaustive search over all 8¹⁰ sign choices for the ten triples of a five-element set finds no unsatisfiable one. Beyond the published range we compute the threshold t(a)=min{b:Ka(a, b) is not totally satisfiable} for a=2,…,8, obtaining t=4,6,7,8,9,11,12, and we compare it with the elementary counting bound m(a)=min{b:C(b, a) ≥ 2ᵃ}: the two agree at every computed a except a=3, and a=3 is exactly the cell the published table gets wrong. Every result stated in this abstract is machine-checked in Lean 4, in a development that declares no axiom of its own and contains no sorry; the reproduction of the published table and both formerly unknown cells are checked by the kernel outright, the corrected cell and the thresholds for a ≥ 6 by the compiled evaluator.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
1cdcb119fd6295005ec1f10478c7a4ee709d88082b770c32a107ba9917be69e3
Claim ledger
Stated results
GU1routine2026-09-03
Total satisfiability of a simple hypergraph is equivalent to the non-existence of a covering of the Boolean cube by one cylinder per edge – both directions, over arbitrary total assignments
GU2candidate2026-09-03
K(4,7) is NOT totally satisfiable – a cell arXiv:2105.11390v1 prints as unknown
GU3candidate2026-09-03
K(5,7) IS totally satisfiable – the second cell arXiv:2105.11390v1 prints as unknown
GU4candidate2026-09-03
K(3,5) IS totally satisfiable – arXiv:2105.11390v1 prints this cell as boldface unsat, and the printed cell is wrong
GU5known data2026-09-03
Every cell of the table of complete uniform hypergraphs printed in arXiv:2105.11390v1, recomputed in the Lean kernel
GU6routine2026-09-03
The pruned complete search for a covering – capacity cut plus normalisation of one edge's pattern by variable negation – is sound and complete
GU7candidate2026-09-03
The threshold sequence t(a) = 4, 6, 7, 8, 9, 11, 12 for a = 2..8, where t(a) is the least b with K(a,b) not totally satisfiable; each entry as a sat/unsat pair
GU8candidate2026-09-03
t(a) equals the counting bound m(a) = minb: C(b,a) >= 2ᵃ at a = 2,4,5,6,7,8 and NOT at a = 3, where C(5,3) = 10 >= 8 = 2³ yet K(3,5) is totally satisfiable
GU9known2026-09-03
The ten satisfiability claims arXiv:2105.11390v1 makes about named graphs – K₄, butterfly, book, bowtie unsatisfiable; K₄ - e, C₄, C₃, the tetrahedron's faces and both triangulations of the triangular prism totally satisfiable – all reproduce
GU10routine2026-09-03
Negative controls: not every K(3,b) is totally satisfiable; not every K(a,b) with b > a fails; C(b,a) >= 2ᵃ does NOT imply unsatisfiability; K(4,7) also carries satisfiable Cnfs; the empty hypergraph is vacuously totally satisfiable; and a structural control that K(a,b) really has C(b,a) pairwise distinct a-element edges
GU11known2026-09-03
Total satisfiability is closed under sub-hypergraphs, so t(a) is a genuine threshold: K(3,b) is totally satisfiable for every b <= 5
GU12routine2026-09-03
t(9) >= 13: K(9,12) is totally satisfiable
GU13measurement2026-09-03
The K(9,13) frontier, priced and parked: randomized greedy (200 restarts, 26.0 s) leaves 49 of 8192 points uncovered, greedy plus local search (40 restarts, 18.9 s) leaves 46, and the natural SAT encoding is 5,857,280 auxiliary variables and about 52.7M clauses, roughly 2 GB of DIMACS before any solving
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Source. Vaibhav Karve and Anil N. Hirani, *GraphSAT — a decision problem connecting satisfiability and graph theory*, arXiv:2105.11390, submitted 24 May 2021, v1 only (checked live 2026-09-02, no journal reference), primary math.CO, cross-listed cs.DM and math.LO. Companion: arXiv:1812.10849, *The complete set of minimal simple graphs that support unsatisfiable 2-CNFs*.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7