## 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):
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

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