Wednesday Night Hack #11 - Experimenting with PyEDA

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!).