# redund.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Redundant (implied) cardinality constraints: for an outer vertex x and a group W other than
# its own, the number of outer y adjacent to x and having an H-neighbour in W is at most |W|
# (each z in W has at most one common neighbour with x, and z has none through N(v)).
from pysat.card import CardEnc, EncType
def red_clauses(k, E, pool):
    g = k-2; ng = k+1; N = k*k
    def x(G, i): return k + 2 + g*(G-1) + i
    def ed(a, b): return E[(min(a, b), max(a, b))]
    outer = list(range(k+2, N))
    grp = {x(G, i): G for G in range(1, ng+1) for i in range(g)}
    cl = []
    hasnb = {}
    for y in outer:
        for W in range(1, ng+1):
            lits = [ed(y, z) for z in outer if grp[z] == W and z != y]
            hv = pool.id(('hn', y, W)); hasnb[(y, W)] = hv
            cl.append([-hv] + lits)
            for l in lits: cl.append([hv, -l])
    for xx in outer:
        for W in range(1, ng+1):
            if W == grp[xx]: continue
            ps = []
            for y in outer:
                if y == xx: continue
                p = pool.id(('p', xx, y, W))
                cl.append([-p, ed(xx, y)]); cl.append([-p, hasnb[(y, W)]])
                cl.append([p, -ed(xx, y), -hasnb[(y, W)]])
                ps.append(p)
            cl += CardEnc.atmost(ps, bound=g, vpool=pool, encoding=EncType.seqcounter).clauses
    return cl