solve over adb

solve.py

import os

os.system("adb exec-out screencap -p > screen.png")

from PIL import Image
img = Image.open("screen.png")
xi = 32
yi = 240
delta = 6
for j in xrange(12):
    for i in xrange(12):
        area = (5+xi+i*80+(i*delta), 5+yi+j*80+j*delta, (-10)+xi+(i+1)*80+(i*delta), (-10)+yi+(j+1)*80+(j*delta) )
        cropped_img = img.crop(area)
        cropped_img.save("out/%d-%d.png" % (i,j))

from subprocess import Popen, PIPE, STDOUT
import string
game = ["." for i in xrange(144)]
for i in xrange(12):
    for j in xrange(12):
        p = Popen(['gocr','-c','01','-i','out/%d-%d.png' % (i,j)], stdout=PIPE, stdin=PIPE, stderr=STDOUT)
        stdout = p.communicate()[0]
        if "no boxes found" in stdout:
            game[j*12+i] = "."
            continue
        if "0" == stdout.strip() or "o" == stdout.strip() or "O" == stdout.strip():
            game[j*12+i] = "0"
        if "1" == stdout.strip():
            game[j*12+i] = "1"

for i in xrange(12):
    for j in xrange(12):
        print game[i*12+j],
    print ""
size = 12
# setup variables and solver
import z3

vs = [(r,c) for r in range(size) for c in range(size)]

v  = [[z3.BitVec('v%d%d' % (r,c),8)  for c in range(size)] for r in range(size)]

# add game constraints
game = filter(lambda x:x in '01.', game)
assert size*size == len(game)
s = z3.Solver()
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(size)]
def col(n):   return [(i, n) for i in range(size)]

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(size):
    s.add(z3.Sum([v[r][c] for r,c in row(i)]) == (size//2))
    s.add(z3.Sum([v[r][c] for r,c in col(i)]) == (size//2))

for i in xrange(size):
    for j in xrange(size-2):
        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(size)]))
s.add(z3.Distinct([z3.Concat([v[r][c] for r,c in col(i)]) for i in xrange(size)]))


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

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

for r,c in vs:
    if game[r*12+c] == "1" or game[r*12+c] == "0":
        continue
    if sol[r][c] == 0:
        os.system("adb shell input tap %d %d" % ((xi+40)+c*86,(yi+40)+r*86))
    if sol[r][c] == 1:
        os.system("adb shell input tap %d %d" % ((xi+40)+c*86,(yi+40)+r*86))
        os.system("adb shell input tap %d %d" % ((xi+40)+c*86,(yi+40)+r*86))