#!/usr/bin/env python3
"""
Ridiculously Easy SAT Problem
by Javantea
Aug 13, 2015

SAT problems are designed to take computationally difficult problems and solve 
them in a reasonable amount of time.

This solves the problem quite quickly. Let's see if we can trick it by changing 
the values.

time python3 ../easy_problem1a.py 
Not satisfiable.

real    0m1.518s
user    0m1.476s
sys     0m0.041s

Fixed. Ran out of memory. Darn... Limit it to 16 bits? No! Hahaha.
Didn't even get to the minisat part... Need some solution.

time python3 ../easy_problem1a1.py 
^CTraceback (most recent call last):
  File "../easy_problem1a1.py", line 72, in <module>
    exp_eq &= -((((vars_x[i] ^ vars_k[i]) & vars_m[i]) ^ vars_x[i]) ^ vars_cmp[i])
  File "/home/sat/satve/lib64/python3.3/site-packages/satispy-1.0a5-py3.3.egg/satispy/cnf.py", line 96, in __neg__
^C
real    2m1.338s
user    1m17.782s
sys     0m3.508s

See how negating produces awfully redundant expressions?
>>> tmp = (a^b)
>>> str(tmp)
'(b | a) & (-b | -a)'
>>> str(-tmp)
'(-b | b) & (b | -a) & (-b | a) & (a | -a)'

If you are not seeing the blatently obvious redundancy here, (-b | b) and 
(-a | a) is the same as saying: Either b or not b. Either a or not a. Yeah, 
that's the only two options. You can trim these using reduceCnf.

"""
from __future__ import print_function
import satispy
import sys
Cnf = satispy.Cnf
Variable = satispy.Variable

bits = 64

vars_x = [satispy.Variable('x%i' % i) for i in range(bits)]

#For this to work... we need to set v and w's constants.

k = 32

vars_k = [satispy.Variable('k%i' % i) for i in range(bits)]

exp_k = satispy.Cnf()
for i in range(bits):
	if k & (1<<i):
		exp_k &= vars_k[i]
	else:
		exp_k &= -vars_k[i]
	#end if
#next i

m = 99
vars_m = [satispy.Variable('m%i' % i) for i in range(bits)]

exp_m = satispy.Cnf()
for i in range(bits):
	if m & (1<<i):
		exp_m &= vars_m[i]
	else:
		exp_m &= -vars_m[i]
	#end if
#next i

expected_output = 0x3334
if len(sys.argv) > 1: expected_output = int(sys.argv[1])

vars_cmp = [satispy.Variable('cmp%i' % i) for i in range(bits)]

exp_cmp = satispy.Cnf()
for i in range(bits):
	if expected_output & (1<<i):
		exp_cmp &= vars_cmp[i]
	else:
		exp_cmp &= -vars_cmp[i]
	#end if
#next i

exp_eq = satispy.Cnf()
for i in range(bits):
	#v_exp = vars_x[i] ^ vars_k[i]
	#w_exp = v_exp & vars_m[i]
	#out_exp = w_exp ^ vars_x[i]
	# This line eats all memory. When I don't negate, it doesn't.
	#exp_eq &= -(out_exp ^ vars_cmp[i])
	exp_eq &= -((((vars_x[i] ^ vars_k[i]) & vars_m[i]) ^ vars_x[i]) ^ vars_cmp[i])
	#print(len(exp_eq.dis))
#next i

solution_cnf = exp_k & exp_m & exp_eq & exp_cmp
print(len(solution_cnf.dis))

io = satispy.io.DimacsCnf()
open('easy_problem1a.cnf', 'w').write(io.tostring(solution_cnf))
solver = satispy.solver.Minisat()
res = solver.solve(solution_cnf)
if res.success:
	print('\n'.join(['%s %r' % (v.name, res[v]) for v in vars_x]))
	x = int(''.join([str(int(res[v])) for v in vars_x][::-1]), 2)
	print('x =', x)
elif res.error:
	print(res.error)
else:
	print("Not satisfiable.")
#end if

def f1(x):
	v = x ^ 32
	w = v & 99
	return w ^ x
#end def f1(x)

"""
# reduceCnf Validator
import satispy
satispy.cnf.cnfClass = satispy.NaiveCnf
a = satispy.Variable('a')
b = satispy.Variable('b')
c = satispy.Variable('c')
e = satispy.Variable('e')
d = (((a ^ b) & c) ^ e)
print(len(d.dis))
#negd = -d
solver = satispy.solver.Minisat()
res = solver.solve(d)
print('\n'.join(['%s %r' % (v.name, res[v]) for v in [a,b,c,e]]))

import satispy
satispy.cnf.cnfClass = satispy.Cnf
a = satispy.Variable('a')
b = satispy.Variable('b')
c = satispy.Variable('c')
e = satispy.Variable('e')
d = (((a ^ b) & c) ^ e)
print(len(d.dis))
negd = -d
print(len(negd.dis))
solver = satispy.solver.Minisat()
res = solver.solve(d)
print('\n'.join(['%s %r' % (v.name, res[v]) for v in [a,b,c,e]]))
solver = satispy.solver.Minisat()
res = solver.solve(negd)
print('\n'.join(['%s %r' % (v.name, res[v]) for v in [a,b,c,e]]))
"""

# These three functions are now part of the default Cnf implementation.
def reduceCnf(cnf):
	"""
	I just found a remarkably large bug in my SAT solver and found an interesting workaround.
	Remove all b | -b
	(-b | b) & (b | -a) & (-b | a) & (a | -a)
	becomes 
	(b | -a) & (-b | a)
	Success ?!
	Remove all (-e) & (-e)
	(-e | a) & (-e | a) & (-e | a) & (-e | a)
	becomes
	(-e | a)
	(-b | b | c) becomes nothing, not (c)
	"""
	output = satispy.Cnf()
	for x in cnf.dis:
		dont_add = False
		for y in x:
			for z in x:
				if z == -y:
					dont_add = True
					break
				#end if
			#next z
			if dont_add: break
		#next y
		if dont_add: continue
		# TODO: Is this necessary anymore? Probably not. Do statistical analysis.
		if x not in output.dis:
			output.dis.append(q)
		#end if
	#next x
	return output
#end def reduceCnf(cnf)

def reduceNegate(cnf):
	cnfs = []
	for d in cnf.dis:
		c = Cnf()
		for v in d:
			#print(str(v))
			c.dis.append(frozenset([-v]))
		x = reduceCnf(c)
		if x not in cnfs:
			cnfs.append(x)
	#print(list(map(str,cnfs)))
	ret = Cnf()
	for cnf_i in cnfs:
		ret = reduceOr(ret, cnf_i)
	return ret
#end def reduceNegate(cnf)

def reduceOr(cnf, other):
	other = Cnf.create_from(other)
	if len(cnf.dis) > 0 and len(other.dis) > 0:
		new_dis = []
		for d1, d2 in [(d1,d2) for d1 in cnf.dis for d2 in other.dis]:
			# TODO: Understand how this works much better.
			#print(d1, d2)
			d3 = d1 | d2
			if d3 not in new_dis:
				new_dis.append(d3)
			#end if
	elif len(cnf.dis) == 0:
		new_dis = other.dis
	else:
		new_dis = cnf.dis
	c = Cnf()
	c.dis = new_dis
	return reduceCnf(c)