# progA2.py
# Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178
# Technical assistance: Claude (Anthropic)
#
# Program A, refined Case II for cubes with two own edges in G_1 (then every group has two own
# edges): G_1 is additionally chosen to maximise c(G) = largest number of vertices of G with the
# same empty cross slot.  With c1 = c(G_1) (read off the cube), every pair of non-partner groups
# is joined by at least 5 - c1 edges.  Author: David Niedbala Giraudin, ORCID 0009-0009-1526-1178.
import json, sys
from collections import Counter
import progA, conc
def write(i, out):
    c = json.load(open('cubesA.json'))[i]
    own = [tuple(p) for p in c['own']]; miss = {int(a): b for a, b in c['miss'].items()}
    assert c['case'] == 'II' and len(own) == 2
    N, pool, E, cl = progA.base('II'); cl += progA.cube_clauses(E, own, miss)
    c1 = max(Counter(miss.values()).values())
    cl += conc.conc_clauses(E, pool, c1)
    with open(out, 'w') as f:
        f.write('p cnf %d %d\n' % (pool.top, len(cl)))
        for x in cl: f.write(' '.join(map(str, x)) + ' 0\n')
    return c1