# symmetry_check.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Checks of the static symmetry breaking used by Program B for the cubes 3, 4, 5 (add_symB.py).
# For every relabelling pi used there:
#   (1) pi is an involution of the 40 outer vertices that maps groups to groups and partner groups
#       to partner groups;
#   (2) pi maps the unit clauses of the cube (the fixed adjacency of group 0) onto themselves;
#   (3) pi fixes groups 1 and 2 pointwise (so the alignment of group 1 to group 2 is untouched).
# Together with the uniform form of all other constraints this makes pi a symmetry of the formula
# (see add_symB.py).  As a further test, the minimum degree of the outer vertices is lowered by one
# (as in falsification_test.py): the relaxed formulas are satisfiable, and for several of their
# models the image under every pi is again a model; the relaxed formulas stay satisfiable when the
# lex-leader clauses are added.
# Pure Python 3 with python-sat, no arguments, about one minute.
import os, sys, json, types
HERE = os.path.dirname(os.path.abspath(__file__)); os.chdir(HERE); sys.path.insert(0, HERE)
from pysat.solvers import Cadical153
from pysat.formula import IDPool
import add_symB, progB
reps = json.load(open('reps39.json'))
ok_all = True
# (1)-(3) on the real formulas
for i in (3, 4, 5):
    rep = reps[i]
    units, top, ncl = add_symB.cube_units(rep)
    for name, vp in add_symB.generators(rep):
        n = len(vp)
        inv = sorted(vp) == list(range(n)) and all(vp[vp[a]] == a for a in range(n))
        grp = add_symB.is_group_map(vp)
        perm = add_symB.edge_perm(vp)
        cube = {(perm[abs(u)] if u > 0 else -perm[abs(u)]) for u in units} == units
        fix12 = all(vp[add_symB.idx[(G, p)]] == add_symB.idx[(G, p)] for G in (1, 2) for p in range(5))
        ok = inv and grp and cube and fix12
        ok_all &= ok
        print('B%d %-7s involution %s, groups and partners preserved %s, cube literals preserved %s, '
              'groups 1 and 2 fixed %s' % (i, name, inv, grp, cube, fix12), flush=True)
# relaxed formulas (minimum degree of the outer vertices lowered by one)
src = open(os.path.join(HERE, 'enc_slots.py')).read()
assert src.count('bound=k-1,') == 1
mod = types.ModuleType('enc_slots'); mod.__file__ = os.path.join(HERE, 'enc_slots.py')
exec(compile(src.replace('bound=k-1,', 'bound=k-2,'), 'enc_slots_relaxed', 'exec'), mod.__dict__)
sys.modules['enc_slots'] = mod
del sys.modules['progB']
import progB as progB_relaxed
V, idx, var, p2, c2 = mod.model(7)
for i in (3, 4, 5):
    rep = reps[i]
    pool, cl, case = progB_relaxed.build(rep)
    gens = add_symB.generators(rep)
    s = Cadical153(bootstrap_with=cl)          # enumerates models (with blocking clauses)
    t = Cadical153(bootstrap_with=cl)          # tests the images
    for trial in range(4):
        if not s.solve():
            print('B%d relaxed: no model' % i, flush=True); ok_all = False; break
        m = set(l for l in s.get_model() if l > 0)
        E = {(a, b) for (a, b), x in var.items() if x in m}
        res = []
        for name, vp in gens:
            Ep = {(min(vp[a], vp[b]), max(vp[a], vp[b])) for (a, b) in E}
            ok = t.solve(assumptions=[x if (a, b) in Ep else -x for (a, b), x in var.items()])
            res.append('%s %s' % (name, 'model' if ok else 'NOT A MODEL'))
            ok_all &= ok
        print('B%d relaxed, model %d: images: %s' % (i, trial, ', '.join(res)), flush=True)
        s.add_clause([-x if (a, b) in E else x for (a, b), x in var.items()])
    s.delete(); t.delete()
    p = IDPool(start_from=pool.top + 1)
    sb = []
    for name, vp in gens:
        sb += add_symB.lex_clauses(add_symB.edge_perm(vp), p, name)
    u = Cadical153(bootstrap_with=cl + sb)
    sat = u.solve(); u.delete()
    ok_all &= sat
    print('B%d relaxed + %d lex-leader clauses: %s' % (i, len(sb), 'satisfiable' if sat else 'UNSATISFIABLE'), flush=True)
print('RESULT:', 'all checks passed' if ok_all else 'SOME CHECK FAILED', flush=True)