#!/usr/bin/env python3

# run: ./gen.py G P W
# for example: ./get.py 7 4 7

import os, sys, time

# in seconds.
TIMEOUT=60*60*24
#TIMEOUT=60*60

G,P,W=int(sys.argv[1]), int(sys.argv[2]), int(sys.argv[3])

#SYMM=False
SYMM=True

N=G*P

"""
G - groups
P - players in group
W - weeks/days
x or N - G*P (total players)

G_ijkl denoting whether player i plays in position j in group k and week l.
i=1..N (all players) (or x)
j=1..P (all players in group)
k=1..G (all groups)
l=1..W (all weeks)

...

...whether player i plays in group k and week l.
(we 'enumerate' all positions):
G'_ikl <-> OR (from j=1 to j=p) G_ijkl
"""

G_vars=[[[[None for l in range(W)] for k in range(G)] for j in range(P)] for i in range(N)]
G_vars_prime=[[[None for l in range(W)] for k in range(G)] for i in range(N)]

cnt=1
for i in range(N):
    for k in range(G):
        for l in range(W):
            G_vars_prime[i][k][l]=cnt
            cnt=cnt+1

for i in range(N):
    for j in range(P):
        for k in range(G):
            for l in range(W):
                G_vars[i][j][k][l]=cnt
                cnt=cnt+1

clauses=[]

"""
        % each player plays at least once each week
        emit(^(i = 1 to N,
               ^(l = 1 to W,
                 v(j = 1 to P,
                   v(k = 1 to G,
                     g(i,j,k,l))))), L),
"""

for i in range(N):
    for l in range(W):
        clause=[]
        for j in range(P):
            for k in range(G):
                clause.append(G_vars[i][j][k][l])
        clauses.append(clause)

"""
        % each player plays at most once in the same group
        emit(^(i = 1 to N,
               ^(l = 1 to W,
                 ^(j = 1 to P,
                   ^(k = 1 to G,
                     ^(m = j+1 to P,
                       g(i,j,k,l) => \g(i,m,k,l)))))), L),
"""

for i in range(N):
    for l in range(W):
        for j in range(P):
            for k in range(G):
                for m in range(j+1, P):
                    clauses.append([-G_vars[i][j][k][l], -G_vars[i][m][k][l]])

"""
        % each player plays at most once per week
        emit(^(i = 1 to N,
               ^(l = 1 to W,
                 ^(j = 1 to P,
                   ^(k = 1 to G,
                     ^(m = k+1 to G,
                       ^(n = 1 to P,
                         g(i,j,k,l) => \g(i,n,m,l))))))), L),
"""

for i in range(N):
    for l in range(W):
        for j in range(P):
            for k in range(G):
                for m in range(k+1, G):
                    for n in range(P):
                        clauses.append([-G_vars[i][j][k][l], -G_vars[i][n][m][l]])

"""
        % in each group, at least one player is the j-th golfer
        emit(^(l = 1 to W,
               ^(k = 1 to G,
                 ^(j = 1 to P,
                   v(i = 1 to N,
                     g(i,j,k,l))))), L),
"""

for l in range(W):
    for k in range(G):
        for j in range(P):
            clause=[]
            for i in range(N):
                clause.append(G_vars[i][j][k][l])
            clauses.append(clause)


"""
        % in each group, at most one player is the j-th golfer
        emit(^(l = 1 to W,
               ^(k = 1 to G,
                 ^(j = 1 to P,
                   ^(i = 1 to N,
                     ^(m = i+1 to N,
                       g(i,j,k,l) => \g(m,j,k,l)))))), L),
"""
for l in range(W):
    for k in range(G):
        for j in range(P):
            for i in range(N):
                for m in range(i+1, N):
                    clauses.append([-G_vars[i][j][k][l], -G_vars[m][j][k][l]])
"""
        % g(i,k,l): player i plays in group k of week l
        % g(i,j,k,l) => g(i,k,l) for all j
        emit(^(l = 1 to W,
               ^(k = 1 to G,
                 ^(j = 1 to P,
                   ^(i = 1 to N,
                     g(i,j,k,l) => g(i,k,l))))), L),
"""
for l in range(W):
    for k in range(G):
        for j in range(P):
            for i in range(N):
                clauses.append([-G_vars[i][j][k][l], G_vars_prime[i][k][l]])

"""
       % g(i,k,l) => g(i,j,k,l) for some j
        emit(^(l = 1 to W,
               ^(k = 1 to G,
                 ^(i = 1 to N,
                   g(i,k,l) => v(j = 1 to P,
                                 g(i,j,k,l))))), L),
"""
for l in range(W):
    for k in range(G):
        for i in range(N):
            clause=[]
            clause.append(-G_vars_prime[i][k][l])
            for j in range(P):
                clause.append(G_vars[i][j][k][l])
            clauses.append(clause)

"""
        % g(x,k,l) ^ g(y,k,l) => -(g(x,k',l') ^ g(y,k',l'))
        emit(^(l = 1 to W,
               ^(k = 1 to G,
                 ^(m = 1 to N,
                   ^(n = m+1 to N,
                     ^(kp = 1 to G,
                       ^(lp = l+1 to W,
                         g(m,k,l) ^ g(n,k,l) =>
                           \ (g(m,kp,lp) ^ g(n,kp,lp)))))))), L),
"""
for l in range(W):
    for k in range(G):
        for m in range(N):
            for n in range(m+1, N):
                for kp in range(G):
                    for lp in range(l+1, W):
                        clauses.append([-G_vars_prime[m][k][l], -G_vars_prime[n][k][l], -G_vars_prime[m][kp][lp], -G_vars_prime[n][kp][lp]])
if SYMM:
    """
            % symmetry breaking constraints
            emit(^(i = 1 to N,
                   ^(j = 1 to P-1,
                     ^(k = 1 to G,
                       ^(l = 1 to W,
                         ^(m = 1 to i,
                           g(i,j,k,l) => \g(m,j+1,k,l)))))), L),
    """
    for i in range(N):
        for j in range(P-1):
            for k in range(G):
                for l in range(W):
                    for m in range(i+1):
                        clauses.append([-G_vars[i][j][k][l], -G_vars[m][j+1][k][l]])
    """
            emit(^(i = 1 to N,
                   ^(k = 1 to G-1,
                     ^(l = 1 to W,
                       ^(m = 1 to i,
                         g(i,1,k,l) => \g(m,1,k+1,l))))), L),
    """
    for i in range(N):
        for k in range(G-1):
            for l in range(W):
                for m in range(i+1):
                    clauses.append([-G_vars[i][0][k][l], -G_vars[m][0][k+1][l]])
    """
            emit(^(i = 1 to N,
                   ^(l = 1 to W-1,
                     ^(m = 1 to i,
                       g(i,2,1,l) => \g(m,2,1,l+1)))), L),
    """
    for i in range(N):
        for l in range(W-1):
            for m in range(i+1):
                clauses.append([-G_vars[i][1][0][l], -G_vars[m][1][0][l+1]])

tmp_cnf_fname="tmp.cnf.%d-%d-%d.%d" % (G, P, W, os.getpid())
tmp_fname="tmp.sol.%d-%d-%d.%d" % (G, P, W, os.getpid())
f=open(tmp_cnf_fname, "w")
f.write ("p cnf %d %d\n" % (cnt-1, len(clauses)))
for clause in clauses:
    tmp=""
    for term in clause:
        tmp=tmp+str(term)+" "
    tmp=tmp+"0"
    f.write (tmp+"\n")
f.close()

start=int(time.time())
os.system ("./kissat --time="+str(TIMEOUT)+" "+tmp_cnf_fname+" > "+tmp_fname)
end=int(time.time())

f=open(tmp_fname,"r")
ar=f.readlines()
f.close()

new_ar=[item.rstrip() for item in ar]

if "s UNSATISFIABLE" in new_ar:
    fname="%d-%d-%d.solution" % (G,P,W)
    f=open(fname, "w")
    f.write("G,P,W=%d,%d,%d\n\n" % (G, P, W))
    f.write("time: %d\n\n" % (end-start))
    f.write ("unsat\n")
    f.close()
    os.unlink(tmp_cnf_fname)
    os.unlink(tmp_fname)
    exit(0)

trues=[]

for line in new_ar:
    if line.startswith("v "):
        tmp=line[2:].split()
        for t in tmp:
            if t[0]!='-':
                i=int(t)
                if i!=0:
                    trues.append(i)
# unpack solution

fname="%d-%d-%d.solution" % (G,P,W)
f=open(fname, "w")

f.write("G,P,W=%d,%d,%d\n\n" % (G, P, W))
f.write("time: %d\n\n" % (end-start))
if len(trues)==0:
    f.write ("no solution. SAT solver timeout?\n")
    f.close()
    exit(0)

for l in range(W): # weeks
    f.write ("* week %d\n" % (l+1))
    t=[]
    for k in range(G):
        tmp=[]
        for i in range(N):
            for j in range(P):
                if G_vars[i][j][k][l] in trues:
                    tmp.append((i+1))
        t.append (tmp)
    f.write (str(t)+"\n")
f.close()

os.unlink(tmp_cnf_fname)
os.unlink(tmp_fname)