Ancillary files for the note "Every C4-free graph on 49 vertices has a vertex of degree at most 6"
Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178.  Technical assistance: Claude (Anthropic).

All scripts are pure Python 3 and take no arguments.  The SAT encoders use the package python-sat
(pip install python-sat).  drat_spot_check.py also needs the executables kissat and drat-trim
(environment variables KISSAT and DRAT_TRIM, or on the PATH).  Run every script from this folder.

Graphs (edge lists in CSV, one edge "a,b" per line, vertices 0..n-1)
  w48.csv          Cayley graph of SD16 x C3, 48 vertices, 7-regular, no 4-cycle    (f(48) = 8)
  relax49.csv      49 vertices, minimum degree 6, no 4-cycle                         (f(49) >= 7)
  hs50.csv         Hoffman-Singleton graph, 50 vertices, 7-regular, girth 5          (f(50) = 8)

Scripts that check something (expected final line in brackets)
  w48_cayley.py               builds the Cayley graph, checks the group axioms and the 4-cycle
                              criterion, writes w48.csv                      [about 0.1 s]
  check_graphs.py             independent checker of the three edge lists    [a few seconds]
  coverage_check_canonical.py the cubes of both programs cover the 39 classes of patterns, exactly
                              once each (canonical forms)                    [about 15 s]
  coverage_check_unionfind.py the same by union-find, no canonical forms     [about 1 min]
  make_formulas.py            rebuilds every formula given to the solvers and compares its SHA-256
                              with formulas_sha256.log (101 formulas, about 1.1 GB in formulas/)
                                                                             [about 2-3 min]
  falsification_test.py       positive control: with the degree bound lowered by one, 17 formulas
                              of both programs (every kind of formula used) become satisfiable
                              and the models decode to C4-free graphs of minimum degree 6
                                                                             [about 3 min]
  symmetry_check.py           checks the relabellings used for the static symmetry breaking of
                              Program B (cubes 3, 4, 5), also on models of relaxed formulas
                                                                             [about 1 min]
  verify_logs.py              reads the logs (folder logs/) of both programs and checks that every
                              cube is refuted by the tree rules of the note  [a few seconds]
  drat_spot_check.py          re-solves a fixed random sample of refuted nodes with DRAT proofs and
                              checks every proof with drat-trim               [about 8-9 min]

Modules (imported by the scripts above)
  Program A : enc_struct.py, symbreak.py, redund.py, tri.py, globsb.py, conc.py, progA.py,
              progA2.py, add_type.py, add_exactA.py
  Program B : enc_slots.py, progB.py, add_symB.py, add_exactB.py
  Logs      : unpack_logs.py

Data
  cubesA.json          the 39 cubes of Program A
  reps39.json          the 39 class representatives of Program B
  formulas_sha256.log  SHA-256 of the formulas that were actually solved
  logs_bundle.log      the folder logs/ packed into one file (the archive may hold at most 99
                       files); unpack_logs.py recreates logs/ and checks every SHA-256, and
                       verify_logs.py and drat_spot_check.py call it first.  Content of logs/:
                       solver logs of both programs (one line per run: node, result, solver seconds;
                       an optional field E or S names the formula variant; a field W or W:<solver>
                       marks the runs distributed as separate tasks to a second computer or to
                       the server (W:cadical-exe, W:cadical-server: CaDiCaL 3.0.1 under a
                       conflict limit), whose literals were regenerated from the logged splits
                       before entry), splits (march_cu cubes), manifests with the SHA-256 of the
                       formulas