#!/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
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<* 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<** 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)
*