# symbreak.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Symmetry-breaking clauses added to the structured model (valid by relabelling inside groups).
import itertools
def sb_clauses(k, E, pool):
    g = k - 2
    ng = k + 1
    def x(G, i): return k + 2 + g*(G-1) + i          # groups numbered 1..k+1
    def ed(a, b): return E[(min(a, b), max(a, b))]
    partner = lambda G: G+1 if G % 2 == 1 else G-1
    cl = []
    def align(ref, w):
        # G_w aligned to G_ref: matched positions of G_w are a prefix, in increasing order of the ref index
        for i, ii in itertools.combinations(range(g), 2):
            for j in range(g):
                for jj in range(j):
                    cl.append([-ed(x(ref, i), x(w, j)), -ed(x(ref, ii), x(w, jj))])
        ys = []
        for j in range(g):
            y = pool.id(('y', ref, w, j)); ys.append(y)
            lits = [ed(x(ref, i), x(w, j)) for i in range(g)]
            cl.append([-y] + lits)
            for l in lits: cl.append([y, -l])
        for j in range(1, g):
            cl.append([-ys[j], ys[j-1]])
    for w in range(1, ng+1):
        if w not in (1, 2):
            align(1, w)
    align(3, 2)
    # own-group matching inside G_1 restricted to pairs (0,1),(2,3),... used in order
    pairs = [(2*t, 2*t+1) for t in range(g//2)]
    for a, b in itertools.combinations(range(g), 2):
        if (a, b) not in pairs:
            cl.append([-ed(x(1, a), x(1, b))])
    for t in range(1, len(pairs)):
        cl.append([-ed(x(1, pairs[t][0]), x(1, pairs[t][1])), ed(x(1, pairs[t-1][0]), x(1, pairs[t-1][1]))])
    return cl