z3py Vietnamese Math Puzzle Solver

gistfile1.py

from z3 import *

# Vietnamese Math Puzzle for 8-Year-Olds Solver
# http://gizmodo.com/can-you-solve-this-vietnamese-math-puzzle-for-8-year-ol-1705734738

s = Solver()

cv = [Int('cv%s'%i) for i in range(9)]

for v in cv:
    s.add(v > 0, v < 10) # must be value between 1-9

s.add(cv[0]+13*cv[1]/cv[2]+cv[3]+12*cv[4]-cv[5]-11+cv[6]*cv[7]/cv[8]-10==66)

s.add(Distinct(cv)) # no cheating - use distinct values
if s.check() == sat:
    print s.model()