# add_symB.py -- Program B: static symmetry breaking (lex-leader) for the Case II cubes B3, B4, B5.
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178.  Technical assistance: Claude (Anthropic).
#
# A relabelling of the outer vertices that maps groups to groups, preserves the partner pairs, and
# maps the fixed adjacency of group 0 (the cube) to itself, preserves every constraint of the
# formula of progB.py: the conditions (a)-(f), the pigeonhole, triangle and Case II constraints are
# stated uniformly for all vertices and groups, the alignment clauses of the groups 2..7 to group 0
# are implied by the cube literals, and the relabellings below fix group 1 and group 2 pointwise,
# so the alignment of group 1 to group 2 is untouched.  Hence such a relabelling maps solutions to
# solutions, and adding "E <= E o pi" (lexicographic order of the edge variables, in index order)
# for some of these relabellings pi keeps at least one solution of every orbit (the least one).
# Relabellings used (groups numbered 0..7, partner of G = G + 1 - 2 (G mod 2); positions 0..4):
#   swap of the vertices 0,1 of group 0 together with positions 0,1 of every group w whose matching
#   to group 0 is the identity and whose positions 0,1 are matched to the vertices 0,1;
#   swaps of whole groups (position by position) among 4,5,6,7 preserving the pairs {4,5},{6,7},
#   when the adjacency of group 0 to these groups is the same.
# Each relabelling is checked below against the cube literals of the formula before use.
import itertools, json
from pysat.formula import IDPool
from enc_slots import model
import progB
k = 7; g = 5
V, idx, var, pool0, cl0 = model(k)
n = len(V)
def h(a, b): return var.get((min(a, b), max(a, b)))
def partner(G): return G + 1 - 2 * (G % 2)
def edge_perm(vp):
    """vertex permutation (list) -> permutation of the edge variables (dict var -> var)"""
    out = {}
    for (a, b), x in var.items():
        y = h(vp[a], vp[b]); assert y is not None
        out[x] = y
    return out
def is_group_map(vp):
    for a in range(n):
        for b in range(n):
            if (V[a][0] == V[b][0]) != (V[vp[a]][0] == V[vp[b]][0]): return False
            if (partner(V[a][0]) == V[b][0]) != (partner(V[vp[a]][0]) == V[vp[b]][0]): return False
    return True
def cube_units(rep):
    """the unit clauses on group-0 edges produced by progB for this cube"""
    pool, cl, case = progB.build(rep)
    units = {c[0] for c in cl if len(c) == 1}
    g0 = {x for (a, b), x in var.items() if V[a][0] == 0 or V[b][0] == 0}
    return {u for u in units if abs(u) in g0}, pool.top, len(cl)
def generators(rep):
    gens = []
    miss = {int(p): w - 1 for p, w in rep['miss'].items()}
    ident = [w for w in range(2, 8) if all(miss.get(i) != w for i in range(g))]
    # swap of vertices 0,1 of group 0 (both on the inner edge) with positions 0,1 of identity groups
    if [tuple(e) for e in rep['own']] == [(0, 1)] and miss.get(0) == miss.get(1):
        vp = list(range(n))
        def sw(a, b): vp[a], vp[b] = vp[b], vp[a]
        sw(idx[(0, 0)], idx[(0, 1)])
        for w in ident: sw(idx[(w, 0)], idx[(w, 1)])
        gens.append(('swap01', vp))
    # whole-group swaps among 4..7
    def gswap(pairs):
        vp = list(range(n))
        for A, B in pairs:
            for p in range(g):
                vp[idx[(A, p)]], vp[idx[(B, p)]] = idx[(B, p)], idx[(A, p)]
        return vp
    if 4 in ident and 5 in ident: gens.append(('g45', gswap([(4, 5)])))
    if 6 in ident and 7 in ident: gens.append(('g67', gswap([(6, 7)])))
    if all(w in ident for w in (4, 5, 6, 7)): gens.append(('g46_57', gswap([(4, 6), (5, 7)])))
    return gens
def lex_clauses(perm, pool, tag):
    """E <= E o perm for an involution perm on the edge variables, variables in index order"""
    cl = []
    prev = None
    for x in sorted(perm):
        y = perm[x]
        if y <= x: continue
        # e_prev and x -> y ; e_prev and (x == y) -> e_new
        e = pool.id((tag, x))
        pre = [] if prev is None else [-prev]
        cl.append(pre + [-x, y])
        cl.append(pre + [-x, -y, e])
        cl.append(pre + [x, y, e])
        prev = e
    return cl
def run(i, src, dst):
    rep = json.load(open('reps39.json'))[i]
    units, top, ncl = cube_units(rep)
    hdr = open(src).readline().split()
    assert int(hdr[2]) == top and int(hdr[3]) == ncl, 'formula differs from progB.build'
    pool = IDPool(start_from=top + 1)
    cl = []; names = []
    for name, vp in generators(rep):
        assert sorted(vp) == list(range(n)) and all(vp[vp[a]] == a for a in range(n)), name
        assert is_group_map(vp), name
        perm = edge_perm(vp)
        img = {(perm[abs(u)] if u > 0 else -perm[abs(u)]) for u in units}
        assert img == units, name + ': cube literals not preserved'
        # group 1 and group 2 fixed pointwise (alignment of group 1 to group 2 untouched)
        assert all(vp[idx[(G, p)]] == idx[(G, p)] for G in (1, 2) for p in range(g)), name
        cl += lex_clauses(perm, pool, name); names.append(name)
    with open(src) as f, open(dst, 'w') as out:
        f.readline()
        out.write('p cnf %d %d\n' % (pool.top, ncl + len(cl)))
        for line in f: out.write(line)
        for c in cl: out.write(' '.join(map(str, c)) + ' 0\n')
    return names, len(cl)