# tri.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Implied triangle constraints.  For a vertex x of degree k whose neighbours have degree >= k,
# the vertices within distance 2 number 1 + k + sum(d(y)-1) - 2T(x) <= k*k, where T(x) is the
# number of edges inside N(x); hence T(x) >= 1.  For an outer vertex of degree k+1 the same
# count gives T(x) = (k+1)/2.  Encoded (weakened, always valid): every outer vertex lies on a
# triangle.
import itertools
def tri_clauses(k, E, pool):
    N = k*k
    def ed(a, b): return E[(min(a, b), max(a, b))]
    outer = list(range(k+2, N))
    g = k-2
    grp = lambda x: (x-(k+2))//g
    cl = []
    for x in outer:
        u = 1 + grp(x)                      # the vertex of N(v) attached to x's group
        cands = []
        # triangles x-u-y with y in x's own group (own edge)
        for y in outer:
            if y != x and grp(y) == grp(x):
                cands.append(ed(x, y))
        # triangles x-y-z inside the outer graph
        for y, z in itertools.combinations([w for w in outer if w != x], 2):
            t = pool.id(('tri', x, y, z))
            cl.append([-t, ed(x, y)]); cl.append([-t, ed(x, z)]); cl.append([-t, ed(y, z)])
            cands.append(t)
        cl.append(cands)
    return cl