# falsification_test.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Positive control for both programs.  The formulas of the proof are built exactly as in
# make_formulas.py, except that the lower bound on the degree of the outer vertices is lowered
# by one (minimum degree 6 instead of 7).  Everything else is kept: the cube (pattern of G_1),
# the symmetry breaking, the Case II conditions and the refinements of Section 5.  These relaxed
# formulas must be satisfiable; each model found is decoded into a graph on 49 vertices and
# checked directly (C4-free, minimum degree 6).  This shows that the encodings are not
# unsatisfiable for a trivial reason.
# Pure Python 3 with python-sat, no arguments, about 3 minutes.
import os, sys, json, types, itertools, tempfile
HERE = os.path.dirname(os.path.abspath(__file__)); os.chdir(HERE); sys.path.insert(0, HERE)
from pysat.solvers import Cadical153

def relaxed_module(name, old, new):
    src = open(os.path.join(HERE, name + '.py')).read()
    assert src.count(old) == 1, (name, old)
    mod = types.ModuleType(name)
    mod.__file__ = os.path.join(HERE, name + '.py')
    exec(compile(src.replace(old, new), name + '_relaxed', 'exec'), mod.__dict__)
    sys.modules[name] = mod
    return mod

# relaxed copies of the two base models, installed before the program modules are imported
enc_struct = relaxed_module('enc_struct', 'bound=k-1,', 'bound=k-2,')
enc_slots = relaxed_module('enc_slots', 'bound=k-1,', 'bound=k-2,')
import progA, progA2, add_type, progB, add_symB, add_exactB, add_exactA

def solve_file(path):
    clauses = []
    with open(path) as f:
        f.readline()
        for line in f:
            lits = list(map(int, line.split()))[:-1]
            clauses.append(lits)
    s = Cadical153(bootstrap_with=clauses)
    ok = s.solve()
    model = set(l for l in s.get_model() if l > 0) if ok else None
    s.delete()
    return ok, model

def check_graph(n, edges):
    adj = [set() for _ in range(n)]
    for a, b in edges:
        adj[a].add(b); adj[b].add(a)
    c4 = any(len(adj[a] & adj[b]) >= 2 for a, b in itertools.combinations(range(n), 2))
    return min(len(x) for x in adj), max(len(x) for x in adj), not c4

tmp = tempfile.mkdtemp()
all_ok = True
# ---- Program A ----
N, pool0, E, cl0 = enc_struct.build(7)          # variable numbering of the pairs (same in all A formulas)
cubes = json.load(open('cubesA.json'))
tests_A = [('A0', 0), ('A38', 38), ('R19', 19), ('A35', 35), ('A36c', 36), ('A37c', 37), ('A36E', 36), ('A37E', 37)]
for name, i in tests_A:
    c = cubes[i]
    base = os.path.join(tmp, 'A%d.cnf' % i)
    progA.write(c['case'], [tuple(p) for p in c['own']], {int(a): b for a, b in c['miss'].items()}, base)
    if name.startswith('R'):
        path = os.path.join(tmp, name + '.cnf'); progA2.write(i, path)
    elif name.endswith('c'):
        path = os.path.join(tmp, name + '.cnf'); add_type.run(i, i == 36, base, path)
    elif name.endswith('E'):
        mid = os.path.join(tmp, 'A%dc.cnf' % i); add_type.run(i, i == 36, base, mid)
        path = os.path.join(tmp, name + '.cnf'); add_exactA.run(i, base, mid, path)
    else:
        path = base
    ok, model = solve_file(path)
    if not ok:
        print('Program A, %s relaxed: UNSATISFIABLE (unexpected)' % name, flush=True); all_ok = False; continue
    edges = [ab for ab, v in E.items() if v in model]
    dmin, dmax, c4free = check_graph(N, edges)
    good = c4free and dmin == 6
    all_ok &= good
    print('Program A, %-4s relaxed: SAT, decoded graph: %d vertices, %d edges, degrees %d..%d, %s'
          % (name, N, len(edges), dmin, dmax, 'C4-free' if c4free else 'HAS C4'), flush=True)
# ---- Program B ----
reps = json.load(open('reps39.json'))
tests_B = [(1, ''), (0, ''), (10, ''), (3, ''), (4, ''), (5, ''), (3, 'S'), (4, 'E'), (5, 'E')]
for i, vr in tests_B:
    pool, cl, case = progB.build(reps[i])
    if vr:
        # the formulas B<i>S (static symmetry breaking) and B<i>E (also exact switch variables)
        base = os.path.join(tmp, 'B%d.cnf' % i)
        with open(base, 'w') as f:
            f.write('p cnf %d %d\n' % (pool.top, len(cl)))
            for c in cl: f.write(' '.join(map(str, c)) + ' 0\n')
        path = os.path.join(tmp, 'B%dS.cnf' % i); add_symB.run(i, base, path)
        if vr == 'E':
            p2 = os.path.join(tmp, 'B%dE.cnf' % i); add_exactB.run(i, path, p2); path = p2
        ok, model = solve_file(path)
    else:
        s = Cadical153(bootstrap_with=cl)
        ok = s.solve()
        model = set(l for l in s.get_model() if l > 0) if ok else None
        s.delete()
    if not ok:
        print('Program B, B%d%s relaxed: UNSATISFIABLE (unexpected)' % (i, vr), flush=True); all_ok = False; continue
    V, idx, var, p2, c2 = enc_slots.model(7)        # same variable numbering as inside progB.build
    # whole graph: 0 = v, 1..8 = N(v) with matching (1,2),(3,4),(5,6),(7,8); group g attached to 1+g
    edges = [(0, j) for j in range(1, 9)] + [(1, 2), (3, 4), (5, 6), (7, 8)]
    edges += [(1 + V[t][0], 9 + t) for t in range(len(V))]
    edges += [(9 + a, 9 + b) for (a, b), x in var.items() if x in model]
    dmin, dmax, c4free = check_graph(49, edges)
    good = c4free and dmin == 6
    all_ok &= good
    print('Program B, %-4s relaxed: SAT, decoded graph: 49 vertices, %d edges, degrees %d..%d, %s'
          % ('B%d%s' % (i, vr), len(edges), dmin, dmax, 'C4-free' if c4free else 'HAS C4'), flush=True)
print('RESULT:', 'all relaxed formulas satisfiable, all decoded graphs C4-free with minimum degree 6'
      if all_ok else 'FAILED', flush=True)