# conc.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Case II, cubes with two own edges in G_1: then every group has two own edges (G_1 has the
# fewest), and G_1 is moreover chosen to maximise c(G) = max_W (5 - m(G,W)) over the groups W
# that are not G or its partner (m = number of edges between the two groups).  Hence, with
# c1 = c(G_1) read from the cube, every pair of non-partner groups has m >= 5 - c1.
from pysat.card import CardEnc, EncType
def conc_clauses(E, pool, c1, k=7):
    g = k-2
    xv = lambda Gr, i: k+2+g*(Gr-1)+i
    ed = lambda a, b: E[(min(a, b), max(a, b))]
    partner = lambda Gr: Gr+1 if Gr % 2 == 1 else Gr-1
    cl = []
    if c1 >= g: return cl
    for A in range(1, k+2):
        for B in range(A+1, k+2):
            if B == partner(A): continue
            lits = [ed(xv(A, i), xv(B, j)) for i in range(g) for j in range(g)]
            cl += CardEnc.atleast(lits, bound=g-c1, vpool=pool, encoding=EncType.seqcounter).clauses
    return cl