# enc_struct.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Structured SAT model: C4-free graph on k*k vertices, min degree >= k (k odd),
# with a tight vertex 0 of degree k+1 (forced by parity + counting lemma).
# Module imported by progA.py and add_type.py (no command-line use).
import sys, itertools
from pysat.card import CardEnc, EncType
from pysat.formula import IDPool

def build(k, extra=''):
    N = k*k
    pool = IDPool()
    E = {}
    def e(a, b):
        if a > b: a, b = b, a
        return pool.id(('e', a, b))
    for a in range(N):
        for b in range(a+1, N):
            E[(a, b)] = e(a, b)
    cl = []
    nbr0 = list(range(1, k+2))                       # neighbours of 0
    partner = {}
    for i in range(0, k+1, 2):
        partner[nbr0[i]] = nbr0[i+1]; partner[nbr0[i+1]] = nbr0[i]
    g = k-2
    group = {}
    start = k+2
    for u in nbr0:
        group[u] = list(range(start, start+g)); start += g
    assert start == N
    fixed = {}
    for a in range(N):
        for b in range(a+1, N):
            val = None
            if a == 0:
                val = (b in nbr0)
            elif a in nbr0 and b in nbr0:
                val = (partner[a] == b)
            elif a in nbr0:
                val = (b in group[a])
            if val is not None:
                fixed[(a, b)] = val
                cl.append([E[(a, b)]] if val else [-E[(a, b)]])
    # C4-free: for every 4-set, 3 possible 4-cycles
    lit = lambda a, b: E[(min(a, b), max(a, b))]
    for q in itertools.combinations(range(N), 4):
        a, b, c, d = q
        for cyc in ((a, b, c, d), (a, b, d, c), (a, c, b, d)):
            ed = [(cyc[i], cyc[(i+1) % 4]) for i in range(4)]
            c4 = []
            skip = False
            for (x, y) in ed:
                key = (min(x, y), max(x, y))
                if key in fixed:
                    if not fixed[key]:
                        skip = True; break
                    continue
                c4.append(-E[key])
            if skip: continue
            if not c4:
                raise RuntimeError('fixed part contains C4')
            cl.append(c4)
    # degree constraints for vertices not fully fixed: outer vertices
    for x in range(k+2, N):
        inc = [E[(min(x, y), max(x, y))] for y in range(N) if y != x and (min(x, y), max(x, y)) not in fixed]
        # x already has exactly one fixed neighbour (its u); need total >= k, <= k+1
        enc = CardEnc.atleast(lits=inc, bound=k-1, vpool=pool, encoding=EncType.seqcounter)
        cl.extend(enc.clauses)
        enc = CardEnc.atmost(lits=inc, bound=k, vpool=pool, encoding=EncType.seqcounter)
        cl.extend(enc.clauses)
    return N, pool, E, cl