# Program B (second, independent pipeline).  Author: David Niedbala Giraudin,
# ORCID 0009-0009-1526-1178.  Technical assistance: Claude (Anthropic).
#
# Model: only the graph H on the 40 outer vertices (groups 0..7, partner = g + 1 - 2 (g mod 2)), with the
# conditions (a)-(f) of enc_slots.py.  Symmetry breaking written independently of Program A:
#   alignment of groups 2..7 to group 0 and of group 1 to group 2 (matched positions form a
#   prefix, in increasing order of their partner's index);
#   cube = complete adjacency of group 0 (one canonical representative per orbit, reps39.json);
#   case I  (cube contains a vertex with no missing slot): nothing more;
#   case II (cube has no such vertex): every outer vertex has H-degree k-1 and group 0 has the
#           fewest own edges.
# Implied constraint added (proved in the note, Lemma 6): for an outer vertex x and a group W
# other than its own, at most |W| H-neighbours of x have an H-neighbour in W.
import sys, json, itertools
from pysat.card import CardEnc, EncType
from enc_slots import model
k = 7; g = 5
def build(rep):
    V, idx, var, pool, cl = model(k)
    h = lambda a, b: var.get((min(a, b), max(a, b)))
    X = lambda Gr, p: idx[(Gr, p)]
    n = len(V)
    def align(ref, w):
        for i, ii in itertools.combinations(range(g), 2):
            for j in range(g):
                for jj in range(j):
                    cl.append([-h(X(ref, i), X(w, j)), -h(X(ref, ii), X(w, jj))])
        for j in range(1, g):
            for i in range(g):
                cl.append([-h(X(ref, i), X(w, j))] + [h(X(ref, i2), X(w, j-1)) for i2 in range(g)])
    for w in range(2, 8): align(0, w)
    align(2, 1)
    # implied pigeonhole constraint
    hasn = {}
    for y in range(n):
        for W in range(8):
            lits = [h(y, z) for z in range(n) if V[z][0] == W and z != y and h(y, z)]
            t = pool.id(('hasn', y, W)); hasn[(y, W)] = t
            cl.append([-t] + lits)
            for l in lits: cl.append([t, -l])
    for x in range(n):
        for W in range(8):
            if W == V[x][0]: continue
            ps = []
            for y in range(n):
                e = h(x, y)
                if y == x or not e: continue
                p = pool.id(('pp', x, y, W)); ps.append(p)
                cl.append([-p, e]); cl.append([-p, hasn[(y, W)]]); cl.append([p, -e, -hasn[(y, W)]])
            cl.extend(CardEnc.atmost(ps, bound=g, vpool=pool, encoding=EncType.totalizer).clauses)
    own = [tuple(e) for e in rep['own']]; miss = {int(p): w - 1 for p, w in rep['miss'].items()}
    for i, j in itertools.combinations(range(g), 2):
        l = h(X(0, i), X(0, j)); cl.append([l] if (i, j) in own else [-l])
    matched = {p for e in own for p in e}
    for w in range(2, 8):
        S = sorted(i for i in range(g) if not (i in matched and miss.get(i) == w))
        for i in range(g):
            for j in range(g):
                want = (i in S and S.index(i) == j)
                l = h(X(0, i), X(w, j)); cl.append([l] if want else [-l])
    case = 'I' if any(p not in miss for p in matched) else 'II'
    if case == 'II':
        for x in range(n):
            lits = [h(x, y) for y in range(n) if y != x and h(x, y)]
            cl.extend(CardEnc.atmost(lits, bound=k-1, vpool=pool, encoding=EncType.totalizer).clauses)   # case II: H-degree exactly k-1
        ownl = {Gr: [h(X(Gr, i), X(Gr, j)) for i, j in itertools.combinations(range(g), 2)] for Gr in range(8)}
        s0 = len(own)
        for Gr in range(1, 8):
            # group 0 has the fewest own edges: every other group has at least s0 own edges
            if s0 > 0:
                cl.extend(CardEnc.atleast(ownl[Gr], bound=s0, vpool=pool, encoding=EncType.totalizer).clauses)
        if s0 == 2:
            # refined choice (independent formulation): group 0 maximises the largest number of
            # its vertices sharing one empty cross slot; with c0 that number for the cube, every
            # two non-partner groups are joined by at least 5 - c0 edges.
            from collections import Counter
            c0 = max(Counter(miss.values()).values())
            if c0 < g:
                for A in range(8):
                    for B in range(A+1, 8):
                        if B == (A + 1 - 2 * (A % 2)): continue
                        lits = [h(X(A, i), X(B, j)) for i in range(g) for j in range(g)]
                        cl.extend(CardEnc.atleast(lits, bound=g-c0, vpool=pool, encoding=EncType.totalizer).clauses)

        if s0 == 1:
            # Groups with exactly one own edge xy: the other three vertices have their empty slot
            # in the own group; x, y have empty slots b_x, b_y.  Type: alpha (b_x = b_y), beta
            # (b_x, b_y partner groups), gamma (otherwise).  Group 0 is chosen of highest type
            # (alpha > beta > gamma) among the groups with one own edge.
            mx = sorted(miss.values())
            typ = 'alpha' if mx[0] == mx[1] else ('beta' if (mx[0] + 1 - 2 * (mx[0] % 2)) == mx[1] else 'gamma')
            if typ != 'alpha':
                for A in range(8):
                    two = pool.id(('twoB', A))
                    for c in CardEnc.atleast(ownl[A], bound=2, vpool=pool, encoding=EncType.totalizer).clauses:
                        cl.append(c + [-two])
                    cross = lambda A, B: [h(X(A, i), X(B, j)) for i in range(g) for j in range(g)]
                    others = [B for B in range(8) if B != A and B != (A + 1 - 2 * (A % 2))]
                    for B in others:
                        for c in CardEnc.atleast(cross(A, B), bound=4, vpool=pool, encoding=EncType.totalizer).clauses:
                            cl.append(c + [two])
                    if typ == 'gamma':
                        for B in others:
                            if B % 2 == 0 and (B + 1 - 2 * (B % 2)) in others:
                                for c in CardEnc.atleast(cross(A, B) + cross(A, B + 1 - 2 * (B % 2)), bound=9, vpool=pool, encoding=EncType.totalizer).clauses:
                                    cl.append(c + [two])
    # every outer vertex lies on a triangle: an own-group neighbour (triangle with its vertex of
    # N(v)) or a triangle of H
    for x in range(n):
        opts = [h(x, y) for y in range(n) if y != x and V[y][0] == V[x][0] and h(x, y)]
        nb = [y for y in range(n) if y != x and h(x, y)]
        for y, z in itertools.combinations(nb, 2):
            if h(y, z):
                tv = pool.id(('triB', x, y, z)); opts.append(tv)
                cl.extend([[-tv, h(x, y)], [-tv, h(x, z)], [-tv, h(y, z)]])
        cl.append(opts)
    return pool, cl, case