# started 2018-11-17 by MK.

import sys
from itertools import *    

try:
    args = sys.argv 
    symmetries = {"cyclic":False, "trans":False, "dihedral":False, "alternating":False, "symmetric":False}
    while symmetries.has_key(args[1]):
        symmetries[args[1]] = True
        args = args[1:]
    
    n = int(args[1]) # number of variables
    k = int(args[2]) # length of the shortest cube
    upper = n + 1
    out = None if len(args) == 3 else args[3]
    if out is not None:
        try:
            upper = int(out)
            out = None if len(args) == 4 else args[4]
        except:
            pass
except:

    print """
    type
    
      python naive.py [cyclic|dihedral|alternating|symmetric] <n> <k> [u]
    
    to generate a dimacs encoding of a sat formula which says that there is a DNF tautology with n variables
    in which each cube has length >=k and <u and any two cubes have distinct support. If upper is not given,
    the default n+1 is used. We must have n>=k. 

    If a group keyword is specified, we only search for solutions that are invariant under the action of the
    respective group. 
    """
    sys.exit(1)

binom_cache = dict()    
def binom(n, k):
    try:
        return binom_cache[n, k]
    except:
        if k < 0 or k > n:
            return 0
        if k == 0 or k == n:
            return 1
        binom_cache[n, k] = binom(n - 1, k - 1) + binom(n - 1, k)
        return binom_cache[n, k]

bound = min(n, upper)
while bound > 0 and sum(binom(n, i)*2**(n-i) for i in range(bound, upper)) < 2**n:
    bound -= 1

if min(n, k, upper) <= 0 or upper <= k or k > bound:
    print "c out of bounds"
    print "p 1 1"
    print "1 -1 0"
    exit(0)
    
supports = []
idx2cube = [None]
cube2idx = dict()

# create subcubes
for i in range(k, upper):
    for s in combinations(range(1,n+1), i):
        supports.append(s)
        for sigma in product([-1,1], repeat=i):
            c = tuple(sigma[j]*s[j] for j in range(i))
            cube2idx[c] = len(idx2cube)
            idx2cube.append(c)

# create clauses saying "used cubes must have distinct support"
# we use binary encoding as found in the literature to say "at most one of the cubes sharing the same support may be true"
clauses = []
cnt = len(idx2cube) # variable count
for s in supports:
    B = range(cnt, cnt + len(s)); cnt += len(s) 
    for sigma in product([-1,1], repeat=len(s)):
        c = tuple(sigma[j]*s[j] for j in range(len(s)))
        for j in range(len(s)):
            clauses.append((-cube2idx[c], sigma[j]*B[j]))
                        
# create clauses saying "selected cubes must not be contained in one another"
# (this is not a necessary requirement but can be assumed wlog to reduce the search space)
if False:
    for i in range(1, len(idx2cube)):
        c = list(idx2cube[i])
        rest = list(set(range(1, n + 1)).difference(map(abs, c)))
        for j in range(1, upper - len(c)):
            for s in combinations(rest, j):
                for sigma in product([-1, 1], repeat=j):
                    clauses.append((-i, -cube2idx[tuple(sorted(c + [sigma[l]*s[l] for l in range(j)], key = abs))]))
                
# create clauses saying "every assignment must be covered by at least one cube"
for sigma in product([-1,1], repeat=n):
    c = []
    for j in range(1, len(idx2cube)):
        u = idx2cube[j]
        # if every index (counting from 1) appearing in u has the same sign
        # as the correspondig coordinate of sigma (counting from 0), then u can cover sigma
        if all(sigma[abs(x)-1]*x > 0 for x in u): 
            c.append(j)
    clauses.append(tuple(c))

# create symmetry enforcement clauses, if requested
def cycle2dict(cyc):
    d = dict((i+1,i+1) for i in range(n))
    for i in range(len(cyc)):
        d[cyc[i]] = cyc[(i + 1) % len(cyc)]
    return d
sgn = lambda l : -1 if l < 0 else 1
permute = lambda cube, pi: tuple(sorted([pi[abs(c)]*sgn(c) for c in cube], key=abs))

generators = dict()
generators['cyclic'] = [cycle2dict(range(1,n+1))] # (1,2,...,n)
generators['dihedral'] = [cycle2dict(range(1,n+1)), dict((i+1,n-i) for i in range(n))] # (1,2,...,n) and (1,n)(2,n-1)...
generators['alternating'] = [cycle2dict(range(1,n)), cycle2dict(range(n-2,n+1))] if n>=3 else []
generators['symmetric'] = [cycle2dict(range(1,n+1)), cycle2dict([1, 2])] # (1,2,...,n) and (1,2)
for group in generators:
    if symmetries[group]:
        for j in range(1, len(idx2cube)):
            for pi in generators[group]:
                clauses.append((-j, cube2idx[permute(idx2cube[j], pi)])) # if j then op(j)

# create some symmetry breaking clauses
"""
If we have a solution, permuting the variables and flipping some of them gives another solution.
It also seems reasonable to enforce a cube of length exactly k.
Without loss of generality, we can choose this to be 1 2 3 .. k
"""
clauses.append([cube2idx[tuple(range(1, k + 1))]])
"""
Unit propagation will quickly remove the other cubes with this support from consideration.
For each of the remaining variables k+1...n, we can select one support and a polarization 
and discard all cubes with the same support and the other polarization 
"""
todo = set(range(k + 1, n + 1))
for s in supports:
    i = todo.intersection(s)
    if len(i) > 0:
        todo.difference_update(i)
        for sigma in product([-1,1], repeat=len(s)):
            if any(sigma[j] == -1 and s[j] in i for j in range(len(s))):
                clauses.append([-cube2idx[tuple(sigma[j]*s[j] for j in range(len(s)))]])
        if len(todo) == 0:
            break
"""
We are still free to permute the variables k+1..n. We do so by stipulating that among the
unsigned cubes (1...k-1 i) we choose the one with smallest i (if any)
"""        
for i in range(k + 1, n):
    clauses.append([cube2idx[tuple(range(1, k) + [i])], -cube2idx[tuple(range(1, k) + [i+1])]])

"""
Now we also have the freedom to permute the variables 1..k, and we use it to lex-sort the
signs in the cube (1...k-1 k+1). Remaining degrees of freedom, if there are any, can be 
used to lex-sort the signs in the cube (1...k-1 k+2)
"""
if n > k:
    for sigma in product([-1,1], repeat=k-1):
        if any(sigma[j] > sigma[j+1] for j in range(k-2)):
            clauses.append([-cube2idx[tuple(sigma[j]*(j+1) for j in range(k-1)) + (k+1,)]])
        if n > k + 1:
            for sigma2 in product([-1,1], repeat=k-1):
                if any(sigma[i] == sigma[j] and sigma2[i] > sigma2[j] for i in range(k-1) for j in range(i+1, k-1)):
                    clauses.append([-cube2idx[tuple(sigma[j]*(j+1) for j in range(k-1)) + (k+1,)],
                                    -cube2idx[tuple(sigma2[j]*(j+1) for j in range(k-1)) + (k+2,)]])

clauses.sort(key=len) # move units to front

# print formula
print "p cnf %i %i" % (cnt, len(clauses))
for i in range(1, len(idx2cube)):
    print "c " + str(i) + " = " + str(idx2cube[i])
for c in clauses:
    print " ".join(map(str, c)) + " 0"