# add_exactA.py -- Program A, cubes 36 (gamma) and 37 (beta): exact switch variables and the
# partner-pair bound, appended to cnf/A36c.cnf and cnf/A37c.cnf.
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178.  Technical assistance: Claude (Anthropic).
# add_type.py attaches to every group A a switch two[A] with
#   two[A] -> A has at least 2 inner edges,     not two[A] -> type constraints for A.
# Appended here (same justification as in the note):
#   (1) not two[A] -> A has at most 1 inner edge;
#   (2) for the partner groups A, A' = (1,2), (3,4), (5,6), (7,8): at least 3 inner edges in A and A'.
import itertools
from pysat.formula import IDPool
from pysat.card import CardEnc, EncType
import enc_struct
K = 7; G = K - 2
def xv(Gr, i): return K + 2 + G*(Gr-1) + i
def two_ids(base_top):
    """the variables two[A] of add_type.run, recomputed by the same sequence of allocations"""
    N, pool0, E, cl0 = enc_struct.build(K)
    ed = lambda a, b: E[(min(a, b), max(a, b))]
    pool = IDPool(start_from=base_top + 1)
    two = {}
    for A in range(1, K + 2):
        two[A] = pool.id(('two', A))
        lits = [ed(xv(A, a), xv(A, b)) for a, b in itertools.combinations(range(G), 2)]
        CardEnc.atleast(lits, bound=2, vpool=pool, encoding=EncType.seqcounter)
    return two, E
def run(i, base, src, dst):
    """base: formula A<i> (to locate the variables two[A] of add_type.py), src: A<i>c, dst: A<i>E"""
    two, E = two_ids(int(open(base).readline().split()[2]))
    ed = lambda a, b: E[(min(a, b), max(a, b))]
    own = lambda A: [ed(xv(A, a), xv(A, b)) for a, b in itertools.combinations(range(G), 2)]
    hdr = open(src).readline().split()
    pool = IDPool(start_from=int(hdr[2]) + 1)
    cl = []
    for A in range(1, K + 2):
        for c in CardEnc.atmost(own(A), bound=1, vpool=pool, encoding=EncType.seqcounter).clauses:
            cl.append(c + [two[A]])
    for A in range(1, K + 2, 2):
        cl.extend(CardEnc.atleast(own(A) + own(A + 1), bound=3, vpool=pool, encoding=EncType.seqcounter).clauses)
    with open(src) as f, open(dst, 'w') as g:
        f.readline()
        g.write('p cnf %d %d\n' % (pool.top, int(hdr[3]) + len(cl)))
        for line in f: g.write(line)
        for c in cl: g.write(' '.join(map(str, c)) + ' 0\n')
    return two, len(cl)