On some other related notes :

I ordered this book on constraint based verification. I suspect it will heavy on the computer science, but for $17.99 I couldn't pass it up. I will give it a quick read.

Also, I stumbled on this web site: http://www.personalkanban.com/ - be forewarned, it's new "agey", similar concepts to "GTD". Well worth a read through if you are interested in personal growth. Quoting: "Personal Kanban gives us clarity in our work and our lives by visualizing those tasks, expectations, and commitments we have and helping us prioritize and complete. With only two simple rules, visualize your work and limit your work in progress."

Without further ado, here is the source code to tonight's experiment. Enjoy!

#!/usr/bin/env python2.7 from constraint import * from random import seed class Solver: def __init__(self): self.solver = Problem() self.solver.setSolver(MinConflictsSolver(100)) def add_variable(self, name, length): # Each bit of input variable is in binary domain, internal format is name[bit position] variables = ['{}[{}]'.format(name, i) for i in range(length)] for variable in variables: self.solver.addVariable(variable, [0, 1]) def add_constraint(self, *args): self.solver.addConstraint(*args) def randomize(self): self.solution = self.solver.getSolution() def get_variable(self, name): # generate decimal representation from internal bitwise representation remap = 0 for variable in self.solution: if name in variable: index = variable.replace('[', '_').replace(']', '').split('_')[1] remap += 2**int(index) * int(self.solution[variable]) return remap #seed(1) # fix random seed, if ndeed solver = Solver() # init solver object solver.add_variable('xx', 32) # rand bit [31:0] xx solver.add_variable('yy', 15) # rand bit [15:0] yy # x is EVEN solver.add_constraint(lambda x: x == 0, ['xx[0]']) # x is EVEN # y is ODD solver.add_constraint(lambda x: x == 1, ['yy[0]']) # y is EVEN # solve the problem solver.randomize() # return random solutions for variable xx and yy print(solver.get_variable('xx')) print(solver.get_variable('yy'))