Not much updates lately. Work and life are good. I have probably been working on this for about 2 weeks.
Here is a short write up on an experiment I did using PyEDA for the purpose of developing a "poor-man's" random constraint solver using Python.
At it's core,
PyEDA is a library that provides support for the specification of complex boolean functions.
It provides a very clean interface to
PicoSAT, a popular SAT solver.
The first realization I made was that PyEDA did not support integer values. With the help of the author of PyEDA, the following solution was devised.
You can specify integers using function arrays :
class Int:
def __init__(self, name, width=3, value=None):
self.name = name
self.width = width
if value != None:
self.farray = int2exprs(value, self.width) # a real value
else:
self.farray = exprvars(name, width) # empty variables
A function is array is nothing but an array of boolean variables.
The next step is to add operators.
def __eq__(self, other):
name = "{}eq{}".format(self.name, other.name)
f = Int(name, self.width)
f.farray = farray([Equal(i, j) for i, j in zip(self.farray, other.farray)])
return f
def __add__(self, other):
sum, carry = ripple_carry_add(self.farray, other.farray)
name = "{}add{}".format(self.name, other.name)
f = Int(name, self.width)
f.farray = farray([i & ~(carry[-1] & carry[-2]) for i in sum]) # this is completely incorrect, need to fix overflow issue
return f
A wrapper to the SAT solve function call and a __str__ method :
def satisfy_all(self):
return self.farray.uand().satisfy_all()
def __str__(self):
return self.name + " : " + str(self.farray)
Finally, we need a way to convert the result from the SAT solver back to our Int class.
def from_soln(self, soln):
value = 0
for boolvar in sorted(soln.keys(), reverse=True):
tmp = str(boolvar)
if tmp.startswith(self.name):
value = value | (int(soln[boolvar]) * pow(2,int(tmp[-2])))
return value
I'll conclude this knowledge share post with 3 simple examples :
1.
A == B
This works very well.
>>> a = Int('A', 3)
>>> b = Int('B', 3)
>>> f = (a == b)
>>> for soln in f.satisfy_all():
>>> print("a="+str(a.from_soln(soln))+" b="+str(b.from_soln(soln)))
a=0 b=0
a=4 b=4
a=2 b=2
a=6 b=6
a=1 b=1
a=5 b=5
a=3 b=3
a=7 b=7
2.
F == (A + B)
This works well, but there is an overflow bug that I have chosen not to fix.
>>> a = Int('A', 3)
>>> b = Int('B', 3)
>>> f = Int('F', 3)
>>> g = (f == (a + b))
>>> for soln in g.satisfy_all():
>>> print("a="+str(a.from_soln(soln))+" b="+str(b.from_soln(soln))+" f="+str(f.from_soln(soln)))
a=0 b=0 f=0
a=0 b=4 f=4
a=0 b=2 f=2
a=0 b=6 f=6
a=0 b=1 f=1
[..]
a=2 b=6 f=0 <-- overflow bug
2. F == (A + B), F == 3
The same overflow bug happens here, but I also identified a more serious issue. Since F is kept constant, the SAT solver does not return it's var.
a = Int('A', 3)
b = Int('B', 3)
f = Int('F', 3, 3)
g = (f == (a + b))
for soln in g.satisfy_all():
print("a="+str(a.from_soln(soln))+" b="+str(b.from_soln(soln))+" f="+str(f.from_soln(soln)))
a=0 b=3 f=0 <-- f is not returned by SAT solver
a=2 b=1 f=0
a=1 b=2 f=0
a=4 b=7 f=0 <-- overflow bug
[..]
This concludes my experiment with PyEDA. It was an worthwhile and interesting experiment, but it's time to move on.
As far as "poor-man's" constraint solver goes, this doesn't come close. I would point interested individuals to the
CRAVE project (or, commercial tools!).
