#!/usr/bin/env python3
"""Exact 1-rotational covering minimum via SCIP.
Group Z_(v-1) rotates 0..v-2 and fixes v-1.
Usage: python rot1_scip.py v k t seconds
"""
import sys,json,time
from itertools import combinations
from ortools.linear_solver import pywraplp

def shift(s,v):
    fixed=v-1
    return tuple(sorted(fixed if x==fixed else (x+1)%(v-1) for x in s))
def orbit(s,v):
    cur=tuple(sorted(s)); out=set()
    for _ in range(v-1): out.add(cur); cur=shift(cur,v)
    return frozenset(out)
def part(v,r):
    d={}
    for s in combinations(range(v),r):
        o=orbit(s,v); d.setdefault(min(o),o)
    return [(q,d[q]) for q in sorted(d)]
def main():
    v,k,t=map(int,sys.argv[1:4]); secs=float(sys.argv[4])
    T=part(v,t); K=part(v,k); tm={s:i for i,(_,o) in enumerate(T) for s in o}
    cover=[]
    for rep,o in K: cover.append({tm[tuple(sorted(q))] for q in combinations(rep,t)})
    solver=pywraplp.Solver.CreateSolver("SCIP"); solver.SetTimeLimit(int(secs*1000))
    x=[solver.BoolVar(f"x{j}") for j in range(len(K))]
    for i in range(len(T)): solver.Add(sum(x[j] for j in range(len(K)) if i in cover[j])>=1)
    solver.Minimize(sum(len(K[j][1])*x[j] for j in range(len(K))))
    st=time.time(); status=solver.Solve(); el=time.time()-st
    names={solver.OPTIMAL:"OPTIMAL",solver.FEASIBLE:"FEASIBLE",solver.INFEASIBLE:"INFEASIBLE",solver.UNBOUNDED:"UNBOUNDED",solver.ABNORMAL:"ABNORMAL",solver.NOT_SOLVED:"NOT_SOLVED"}
    out={"cell":[v,k,t],"group":f"Z_{v-1} fixes {v-1}","status":names.get(status,str(status)),"objective":None if status not in (solver.OPTIMAL,solver.FEASIBLE) else solver.Objective().Value(),"best_bound":solver.Objective().BestBound(),"wall_time_seconds":el,"nodes":solver.nodes(),"iterations":solver.iterations(),"t_orbits":len(T),"block_orbits":len(K)}
    if status in (solver.OPTIMAL,solver.FEASIBLE): out["base_blocks"]=[list(K[j][0]) for j in range(len(K)) if x[j].solution_value()>0.5]
    print(json.dumps(out,indent=1)); json.dump(out,open(f"rot1_scip_{v}_{k}_{t}.json","w"),indent=1)
if __name__=="__main__":main()