# globsb.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Further valid symmetry breaking: choice of the reference group G_1 and of the order of the
# other partner pairs.  Uses an exact unary counter (both directions) for small sums.
import itertools
def unary(lits, pool, tag, cl):
    # returns u[1..n] with u[j] <-> (sum lits >= j), via a totalizer with equivalences
    def tot(ls, name):
        if len(ls) == 1:
            return [ls[0]]
        h = len(ls)//2
        A = tot(ls[:h], name+'a'); B = tot(ls[h:], name+'b')
        n = len(A)+len(B)
        R = [pool.id((tag, name, j)) for j in range(1, n+1)]
        for i in range(len(A)+1):
            for j in range(len(B)+1):
                if i+j >= 1:   # (A>=i & B>=j) -> R>=i+j
                    c = [R[i+j-1]]
                    if i: c.append(-A[i-1])
                    if j: c.append(-B[j-1])
                    cl.append(c)
                if i+j < n:    # (A<=i & B<=j) -> R<=i+j  i.e. (not A>=i+1 & not B>=j+1) -> not R>=i+j+1
                    c = [-R[i+j]]
                    if i < len(A): c.append(A[i])
                    if j < len(B): c.append(B[j])
                    cl.append(c)
        return R
    return tot(lits, 'r')
def geq(U, V, cl):
    # sum(U) >= sum(V) for unary vectors of equal length
    for j in range(len(V)):
        cl.append([-V[j], U[j]])
def glob_clauses(k, E, pool):
    g = k-2; ng = k+1
    def x(G, i): return k + 2 + g*(G-1) + i
    def ed(a, b): return E[(min(a, b), max(a, b))]
    cl = []
    own = {}
    for G in range(1, ng+1):
        own[G] = unary([ed(x(G, i), x(G, j)) for i in range(g) for j in range(i+1, g)], pool, ('own', G), cl)
    for G in range(2, ng+1):
        geq(own[1], own[G], cl)
    m = {}
    for w in range(3, ng+1):
        m[w] = unary([ed(x(1, i), x(w, j)) for i in range(g) for j in range(g)], pool, ('m', w), cl)
    for w in range(3, ng+1, 2):
        geq(m[w], m[w+1], cl)
    for w in range(3, ng-1, 2):
        geq(m[w], m[w+2], cl)
    return cl