# add_exactB.py -- Program B, cubes 4 and 5 (Case II, one inner edge in group 0, types beta and gamma):
# exact switch variables and the partner-pair bound.
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178.  Technical assistance: Claude (Anthropic).
#
# In progB.py a switch variable two(A) is attached to every group A with the clauses
#   two(A) -> A has at least 2 inner edges,    not two(A) -> type constraints for A.
# Appended here:
#   (1) not two(A) -> A has at most 1 inner edge.  Every solution of the formula of progB.py remains a
#       solution after setting two(A) := [A has at least 2 inner edges]: a group with 1 inner edge
#       satisfies the type constraints (G_1 has the highest type), and every group has >= 1 inner
#       edge.  So the formula stays satisfiable if it was; the switch now splits the cases exactly.
#   (2) for every pair of partner groups A, A': at least 3 inner edges in A and A' together
#       (Lemma 7 of the note, partner pairs, Case II).
import itertools, json
from pysat.formula import IDPool
from pysat.card import CardEnc, EncType
import progB
g = 5
def extra(two_ids, top):
    """clauses (1) and (2); two_ids[A] = variable two(A) of progB.build; fresh variables after top"""
    from enc_slots import model
    V, idx, var, p0, c0 = model(7)
    h = lambda a, b: var.get((min(a, b), max(a, b)))
    X = lambda G, p: idx[(G, p)]
    own = lambda A: [h(X(A, i), X(A, j)) for i, j in itertools.combinations(range(g), 2)]
    cl = []
    new = IDPool(start_from=top + 1)
    for A in range(8):
        two = two_ids[A]
        for c in CardEnc.atmost(own(A), bound=1, vpool=new, encoding=EncType.seqcounter).clauses:
            cl.append(c + [two])
    for A in range(0, 8, 2):
        cl.extend(CardEnc.atleast(own(A) + own(A + 1), bound=3, vpool=new, encoding=EncType.seqcounter).clauses)
    return cl, new
def run(i, src, dst):
    rep = json.load(open('reps39.json'))[i]
    pool, cl0, case = progB.build(rep)
    hdr = open(src).readline().split()
    two_ids = [pool.obj2id[('twoB', A)] for A in range(8)]
    cl, new = extra(two_ids, int(hdr[2]))
    with open(src) as f, open(dst, 'w') as out:
        f.readline()
        out.write('p cnf %d %d\n' % (new.top, int(hdr[3]) + len(cl)))
        for line in f: out.write(line)
        for c in cl: out.write(' '.join(map(str, c)) + ' 0\n')
    return len(cl)