Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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 ""),
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement