# enc_slots.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Second, independent model (different variables and constraints than enc_struct.py):
# only the graph H on the outer vertices is modelled, with the conditions derived by hand
# from the tight-vertex lemma, written directly (no generic 4-cycle enumeration over all
# 49 vertices).  Outer vertex = (group G, position p), groups 0..k, partner(G) = G + 1 - 2 (G mod 2).
# Conditions on H (all derived from C4-freeness of the whole graph):
#  (a) at most one H-neighbour inside its own group;
#  (b) no H-edge between partner groups;
#  (c) at most one H-neighbour inside any other group;
#  (d) two vertices of the same group have no common H-neighbour;
#  (e) H has no 4-cycle;
#  (f) H-degree of every outer vertex is k-1 or k.
import sys, itertools
from pysat.formula import IDPool
from pysat.card import CardEnc, EncType

def model(k):
    g = k - 2
    ng = k + 1
    V = [(G, p) for G in range(ng) for p in range(g)]
    idx = {v: i for i, v in enumerate(V)}
    pool = IDPool()
    var = {}
    cl = []
    for a, b in itertools.combinations(range(len(V)), 2):
        Ga, Gb = V[a][0], V[b][0]
        if Gb == (Ga + 1 - 2 * (Ga % 2)):
            continue                                  # (b): variable never created
        var[(a, b)] = pool.id(('h', a, b))
    def h(a, b):
        return var.get((min(a, b), max(a, b)))
    # (a),(c): at most one neighbour per group
    for a in range(len(V)):
        for G in range(ng):
            lits = [h(a, b) for b in range(len(V)) if b != a and V[b][0] == G and h(a, b)]
            for l1, l2 in itertools.combinations(lits, 2):
                cl.append([-l1, -l2])
    # (d): same-group vertices share no H-neighbour
    for a, b in itertools.combinations(range(len(V)), 2):
        if V[a][0] != V[b][0]:
            continue
        for c in range(len(V)):
            if c in (a, b): continue
            l1, l2 = h(a, c), h(b, c)
            if l1 and l2:
                cl.append([-l1, -l2])
    # (e): no 4-cycle in H
    for q in itertools.combinations(range(len(V)), 4):
        a, b, c, d = q
        for cyc in ((a, b, c, d), (a, b, d, c), (a, c, b, d)):
            ls = [h(cyc[i], cyc[(i+1) % 4]) for i in range(4)]
            if all(ls):
                cl.append([-l for l in ls])
    # (f)
    for a in range(len(V)):
        lits = [h(a, b) for b in range(len(V)) if b != a and h(a, b)]
        cl += CardEnc.atleast(lits, bound=k-1, vpool=pool, encoding=EncType.totalizer).clauses
        cl += CardEnc.atmost(lits, bound=k, vpool=pool, encoding=EncType.totalizer).clauses
    return V, idx, var, pool, cl