Wednesday, February 25, 2015

Wednesday Night Hack - Next Two Months

I'll be busy in my spare time for the next 9 weeks.  I decided to sign up for MITx course: "Introduction to Computational Thinking and Data Science".  The cost for verified certificate track was a donation of $50, for which I did not mind paying whatsoever.

Here is the list of lecture topics.  It should be fun!!

  • Plotting
  • Simulations and Random Walks
  • Probability
  • Stochastic Programming and Hashing
  • Monte Carlo Simulations
  • Using Randomness to Solve Non-Random Problems
  • Curve Fitting
  • Knapsack Problem
  • Graphs and Graph Optimization
  • Machine Learning
  • Statistical Fallacies
  • Research videos

Thursday, February 19, 2015

TBT - Run Scener Run (2000)

Again, a collaboration with Joseph Mocanu from 2000.

Though, in fairness, he did most of the heavy lifting on this one.  I missed out on most of (but not all) my frosh week at Ryerson while working on this, totally worth it, lol.  Thanks to Andy Voss for capturing.

Wednesday, February 18, 2015

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): = name
        self.width = width
        if value != None:
            self.farray = int2exprs(value, self.width)  # a real value
            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(,
        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(,
        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 + " : " + 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(
                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!).