# Program A (first pipeline).  Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178.
# Technical assistance: Claude (Anthropic).
#
# Instances for k = 7 (49 vertices).  Vertex 0 = a vertex of degree 8 (it exists, Lemma 4),
# 1..8 = its neighbours with the perfect matching (1,2),(3,4),(5,6),(7,8), groups G_1..G_8 of
# five outer vertices, G_i attached to vertex i.  Two cases:
#   Case I : some outer vertex has degree 8; the reference group G_1 is chosen to contain one.
#   Case II: no outer vertex has degree 8; G_1 is chosen with the fewest own (internal) edges.
# Symmetry breaking common to both cases (valid by relabelling, see the note):
#   - every group G_w, w = 3..8, is aligned to G_1; G_2 is aligned to G_3;
#   - the own edges of G_1 are (0,1),(2,3) in this order of use;
#   - m3>=m4, m5>=m6, m7>=m8, m3>=m5>=m7, where m_w = number of edges between G_1 and G_w.
# A cube fixes the whole adjacency of G_1.
import itertools, json, sys
from pysat.card import CardEnc, EncType
import enc_struct, symbreak, redund, tri, globsb
K = 7; G = K - 2
def xv(Gr, i): return K + 2 + G*(Gr-1) + i
def base(case):
    N, pool, E, cl = enc_struct.build(K)
    ed = lambda a, b: E[(min(a, b), max(a, b))]
    cl += symbreak.sb_clauses(K, E, pool)
    cl += redund.red_clauses(K, E, pool)
    cl += tri.tri_clauses(K, E, pool)
    # m-order (taken from globsb, without the own-max condition)
    m = {}
    for w in range(3, K+2):
        m[w] = globsb.unary([ed(xv(1, i), xv(w, j)) for i in range(G) for j in range(G)], pool, ('m', w), cl)
    for w in range(3, K+2, 2): globsb.geq(m[w], m[w+1], cl)
    for w in range(3, K, 2): globsb.geq(m[w], m[w+2], cl)
    if case == 'II':
        for x in range(K+2, N):
            inc = [ed(x, y) for y in range(K+2, N) if y != x]
            cl += CardEnc.atmost(inc, bound=K-1, vpool=pool, encoding=EncType.seqcounter).clauses
        own = {}
        for Gr in range(1, K+2):
            own[Gr] = globsb.unary([ed(xv(Gr, i), xv(Gr, j)) for i in range(G) for j in range(i+1, G)], pool, ('own', Gr), cl)
        for Gr in range(2, K+2):
            globsb.geq(own[Gr], own[1], cl)          # G_1 has the fewest own edges
    return N, pool, E, cl
def cube_clauses(E, own, miss):
    ed = lambda a, b: E[(min(a, b), max(a, b))]
    cl = []
    for i, j in itertools.combinations(range(G), 2):
        cl.append([ed(xv(1, i), xv(1, j))] if (i, j) in own else [-ed(xv(1, i), xv(1, j))])
    for w in range(3, K+2):
        S = [i for i in range(G) if miss.get(i) != w]
        for i in range(G):
            for j in range(G):
                want = (i in S and S.index(i) == j)
                cl.append([ed(xv(1, i), xv(w, j))] if want else [-ed(xv(1, i), xv(w, j))])
    return cl
def write(case, own, miss, out):
    N, pool, E, cl = base(case)
    cl += cube_clauses(E, own, miss)
    with open(out, 'w') as f:
        f.write('p cnf %d %d\n' % (pool.top, len(cl)))
        for c in cl: f.write(' '.join(map(str, c)) + ' 0\n')