#!/usr/bin/python
"""
	This program can be used to determine the value of h_5(n) for small values of n. 
	(c) 2021 Manfred Scheucher <scheucher@tu-berlin.de>
"""

from itertools import combinations
from sys import argv

if len(argv) == 1:
	print "This program can be used to generate an integer linear program"
	print "to determine whether h_5(n) <= m."
	print
	print "\tpython",argv[0],"[n] [m]"
	print
	print "The generated integer linear program then can be solved,"
	print "for example, using GLPK with the command"
	print
	print "\tglpsol --lp problem_h5_[n]_[m].lp --minisat"
	print
	exit()

holesize = int(argv[1])
n = int(argv[2])
m = int(argv[3])
N = range(n)

all_variables = []
all_variables += [('trip',I) for I in combinations(N,3)]
all_variables += [('extr_ab',I) for I in combinations(N,4)]
all_variables += [('extr_cd',I) for I in combinations(N,4)]
all_variables += [('convpos',I) for I in combinations(N,4)]
all_variables += [('b_inner',I) for I in combinations(N,4)]
all_variables += [('c_inner',I) for I in combinations(N,4)]
all_variables += [('emptytr',I) for I in combinations(N,3)]
all_variables += [('conv5hl',I) for I in combinations(N,holesize)]
all_variables += [('count',(I,k)) for I in combinations(N,holesize) for k in range(m+1)]


all_variables_index = {}

_num_vars = 0
for v in all_variables:
	all_variables_index[v] = _num_vars
	_num_vars += 1

def var(L):	return 1+all_variables_index[L]

def var_trip(*L): return var(('trip',L))
def var_extr_ab(*L): return var(('extr_ab',L))
def var_extr_cd(*L): return var(('extr_cd',L))
def var_convpos(*L): return var(('convpos',L))
def var_b_inner(*L): return var(('b_inner',L))
def var_c_inner(*L): return var(('c_inner',L))
def var_emptytr(*L): return var(('emptytr',L)) 
def var_conv5hl(*L): return var(('conv5hl',L)) 
def var_count(*L): return var(('count',L)) 


constraints = []

for I3 in combinations(N,3):
	if 0 in I3:
		constraints.append([var_trip(*I3)]) # points are ordered around p_0 

# signature functions: forbid invalid configuartions 
for I4 in combinations(N,4):
	I4_triples = list(combinations(I4,3))
	for t1,t2,t3 in combinations(I4_triples,3): # lex. ord. triples t1 < t2 < t3
		for sgn in [+1,-1]:
			constraints.append([sgn*var_trip(*t1),-sgn*var_trip(*t2),sgn*var_trip(*t3)])

# assert extremals of 4 points
for I in combinations(N,4):
	[a,b,c,d] = I
	# if ab extremal, then abc = abd
	constraints.append([-var_extr_ab(*I), var_trip(a,b,c),-var_trip(a,b,d)])
	constraints.append([-var_extr_ab(*I),-var_trip(a,b,c), var_trip(a,b,d)])
	# if ab not extremal, then abc != abd 
	constraints.append([ var_extr_ab(*I), var_trip(a,b,c), var_trip(a,b,d)])
	constraints.append([ var_extr_ab(*I),-var_trip(a,b,c),-var_trip(a,b,d)])

	constraints.append([-var_extr_cd(*I), var_trip(a,c,d),-var_trip(b,c,d)])
	constraints.append([-var_extr_cd(*I),-var_trip(a,c,d), var_trip(b,c,d)])
	constraints.append([ var_extr_cd(*I), var_trip(a,c,d), var_trip(b,c,d)])
	constraints.append([ var_extr_cd(*I),-var_trip(a,c,d),-var_trip(b,c,d)])


for I in combinations(N,4):
	[a,b,c,d] = I
	# if convex position, then ab and cd all extremal 
	constraints.append([-var_convpos(*I),var_extr_ab(*I)])
	constraints.append([-var_convpos(*I),var_extr_cd(*I)])

	# if not convex position, ab or cd is non extremal
	constraints.append([var_convpos(*I),-var_extr_ab(*I),-var_extr_cd(*I)])

	# inner-outer relations of each 4-tuple:
	# either convex, or b is inner, or c is inner (exclusive or!)
	constraints.append([var_b_inner(*I),var_c_inner(*I),var_convpos(*I)])
	constraints.append([-var_b_inner(*I),-var_c_inner(*I)])
	constraints.append([-var_b_inner(*I),-var_convpos(*I)])
	constraints.append([-var_c_inner(*I),-var_convpos(*I)])

	constraints.append([ var_b_inner(*I), var_extr_ab(*I)])
	constraints.append([-var_b_inner(*I),-var_extr_ab(*I)])
	constraints.append([ var_c_inner(*I), var_extr_cd(*I)])
	constraints.append([-var_c_inner(*I),-var_extr_cd(*I)])


# empty triangles
for a,b,c in combinations(N,3):
	# if not empty, then there must be an inner point
	constraints.append(
		 [var_emptytr(a,b,c)]
		+[var_b_inner(a,i,b,c) for i in range(a+1,b)]
		+[var_c_inner(a,b,i,c) for i in range(b+1,c)]
		)

	# if empty, then no containment
	for i in range(a+1,b):
		constraints.append([-var_emptytr(a,b,c),-var_b_inner(a,i,b,c)])
	for i in range(b+1,c):
		constraints.append([-var_emptytr(a,b,c),-var_c_inner(a,b,i,c)])


prevI = None
for I in combinations(N,holesize):
	# if not 5-hole, then
	# there must be 4 points not in convex position
	# or some inner points 
	constraints.append(
		 [var_conv5hl(*I)]
		+[-var_convpos(*J) for J in combinations(I,4)]
		+[-var_emptytr(*J) for J in combinations(I,3)]
		)

	# if 5-hole, then everything must be convex and empty
	for J in combinations(I,4):
		constraints.append([-var_conv5hl(*I),var_convpos(*J)])
	for J in combinations(I,3):
		constraints.append([-var_conv5hl(*I),var_emptytr(*J)])


	# assert count 
	constraints.append([var_count(I,k) for k in range(m+1)])
	for k,l in combinations(range(m+1),2):
		constraints.append([-var_count(I,k),-var_count(I,l)])

	if prevI != None:
		constraints.append([-var_count(prevI,m),-var_conv5hl(*I)])
		for k in range(m):
			constraints.append([-var_count(prevI,k),-var_conv5hl(*I),+var_count(I,k+1)])
			#constraints.append([-var_count(prevI,k),+var_conv5hl(*I),-var_count(I,k+1)])

		for k in range(m+1):
			constraints.append([-var_count(prevI,k),+var_conv5hl(*I),+var_count(I,k)])
			#constraints.append([-var_count(prevI,k),-var_conv5hl(*I),-var_count(I,k)])
			
	else:
		constraints.append([+var_conv5hl(*I),+var_count(I,0)])
		if m > 0:
			constraints.append([-var_conv5hl(*I),+var_count(I,1)])
		else:
			constraints.append([-var_conv5hl(*I)])

	prevI = I

#for I,J in combinations(combinations(range(n),5),2):
#	constraints.append([-var_conv5hl(*I),-var_conv5hl(*J)])

print "Total number of constraints:",len(constraints)


fp = "instance_"+str(holesize)+"_"+str(n)+"_"+str(m)+".in"
#fp = "instance.in"
f = open(fp,"w")
f.write("p cnf "+str(_num_vars)+" "+str(len(constraints))+"\n")
for c in constraints:
	f.write(" ".join(str(v) for v in c)+" 0\n")
f.close()

print "Created CNF-file:",fp