A solver for http://binarypuzzle.com/ puzzles based on z3 ( https://github.com/Z3Prover/z3 )

binarypuzzle.py

game = """
.....1...1
1......0..
..0....0..
.00...0..1
1........1
...0..1...
0....1....
.......0.0
0........0
.0.0.1....
"""

# setup variables and solver
import z3

vs = [(r,c) for r in range(10) for c in range(10)]
v  = [[z3.BitVec('v%d%d' % (r,c),8)  for c in range(10)] for r in range(10)]
s = z3.Solver()

# add game constraints
game = filter(lambda x:x in '01.', game)

for ((r,c), val) in zip(vs, game):
    if val == '.':  s.add(0 <= v[r][c], v[r][c] <= 1)
    else:           s.add(v[r][c] == (int(val)))

# add board contraints
def row(n):   return [(n, i) for i in range(10)]
def col(n):   return [(i, n) for i in range(10)]

def row3(n,m):   return [(n, i) for i in range(m,m+3)]
def col3(n,m):   return [(i, n) for i in range(m,m+3)]

for i in xrange(10):
    s.add(z3.Sum([v[r][c] for r,c in row(i)]) == 5)
    s.add(z3.Sum([v[r][c] for r,c in col(i)]) == 5)

for i in xrange(10):
    for j in xrange(8):
        s.add(z3.Sum([v[r][c] for r,c in row3(i,j)]) <= 2)
        s.add(z3.Sum([v[r][c] for r,c in row3(i,j)]) >= 1)
        s.add(z3.Sum([v[r][c] for r,c in col3(i,j)]) <= 2)
        s.add(z3.Sum([v[r][c] for r,c in col3(i,j)]) >= 1)

s.add(z3.Distinct([z3.Concat([v[r][c] for r,c in row(i)]) for i in xrange(10)]))
s.add(z3.Distinct([z3.Concat([v[r][c] for r,c in col(i)]) for i in xrange(10)]))


# find solution
print s.check()
m   = s.model()
sol = [[m[v[r][c]] for c in range(10)] for r in range(10)]

# print solution
for r,c in vs:
    print str(sol[r][c]) + ("\n" if c==9 else ""),