#!/usr/bin/env python3
"""Exact 1-rotational covering minimum via CP-SAT.
Usage: python rot1_cpsat.py v k t seconds workers
"""
import sys,json
from itertools import combinations
from ortools.sat.python import cp_model

def shift(s,v):
    f=v-1; return tuple(sorted(f if x==f 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]); workers=int(sys.argv[5])
    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)})
    m=cp_model.CpModel(); x=[m.NewBoolVar(f"x{j}") for j in range(len(K))]
    for i in range(len(T)):m.Add(sum(x[j] for j in range(len(K)) if i in cover[j])>=1)
    m.Minimize(sum(len(K[j][1])*x[j] for j in range(len(K))))
    s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=secs; s.parameters.num_search_workers=workers
    status=s.Solve(m); name=s.StatusName(status)
    out={"cell":[v,k,t],"group":f"Z_{v-1} fixes {v-1}","status":name,"optimal":status==cp_model.OPTIMAL,"objective":s.ObjectiveValue(),"best_bound":s.BestObjectiveBound(),"wall_time":s.WallTime(),"branches":s.NumBranches(),"conflicts":s.NumConflicts(),"t_orbits":len(T),"block_orbits":len(K)}
    if status in (cp_model.OPTIMAL,cp_model.FEASIBLE):out["base_blocks"]=[list(K[j][0]) for j in range(len(K)) if s.Value(x[j])]
    print(json.dumps(out,indent=1)); print(s.ResponseStats()); json.dump(out,open(f"rot1_cpsat_{v}_{k}_{t}.json","w"),indent=1)
if __name__=="__main__":main()