# check_graphs.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Independent graph checker (shares no code with the SAT encoders).  For every edge-list file
# below (one edge "a b" per line, vertices 0..n-1) it reports the number of vertices and edges,
# the minimum and maximum degree, the number of pairs of vertices with two or more common
# neighbours (a graph has a 4-cycle if and only if such a pair exists), and the girth when it
# is at least 5.  Pure Python, no arguments.
import os, itertools
HERE = os.path.dirname(os.path.abspath(__file__))
FILES = [
    ("w48.csv", "Cayley graph of SD16 x C3: 48 vertices, 7-regular, no C4 (f(48) = 8)"),
    ("hs50.csv", "Hoffman-Singleton graph: 50 vertices, 7-regular, girth 5 (f(50) = 8)"),
    ("relax49.csv", "a C4-free graph on 49 vertices with minimum degree 6 (f(49) >= 7)"),
]

def load(path):
    edges = set()
    for line in open(path):
        p = line.replace(',', ' ').split()
        if len(p) == 2:
            a, b = int(p[0]), int(p[1])
            assert a != b, "loop"
            edges.add((min(a, b), max(a, b)))
    n = 1 + max(max(e) for e in edges)
    adj = [set() for _ in range(n)]
    for a, b in edges:
        adj[a].add(b); adj[b].add(a)
    return n, edges, adj

def girth(n, adj):
    best = None
    for s in range(n):
        dist = {s: 0}; parent = {s: -1}; queue = [s]
        for x in queue:
            for y in adj[x]:
                if y not in dist:
                    dist[y] = dist[x] + 1; parent[y] = x; queue.append(y)
                elif parent[x] != y:
                    c = dist[x] + dist[y] + 1
                    if best is None or c < best: best = c
    return best

for name, what in FILES:
    path = os.path.join(HERE, name)
    if not os.path.exists(path):
        print(name, ": file not found", flush=True); continue
    n, edges, adj = load(path)
    deg = [len(a) for a in adj]
    bad = sum(1 for a, b in itertools.combinations(range(n), 2) if len(adj[a] & adj[b]) >= 2)
    g = girth(n, adj)
    print("%s: %s" % (name, what), flush=True)
    print("   vertices %d  edges %d  min degree %d  max degree %d  pairs with >= 2 common neighbours %d  girth %s  -> %s"
          % (n, len(edges), min(deg), max(deg), bad, g, "C4-free" if bad == 0 else "HAS A C4"), flush=True)