Advertisement
Guest User

Untitled

a guest
Jun 23rd, 2017
48
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 1.47 KB | None | 0 0
  1. game = """
  2. .....1...1
  3. 1......0..
  4. ..0....0..
  5. .00...0..1
  6. 1........1
  7. ...0..1...
  8. 0....1....
  9. .......0.0
  10. 0........0
  11. .0.0.1....
  12. """
  13.  
  14. # setup variables and solver
  15. import z3
  16.  
  17. vs = [(r,c) for r in range(10) for c in range(10)]
  18. v = [[z3.BitVec('v%d%d' % (r,c),8) for c in range(10)] for r in range(10)]
  19. s = z3.Solver()
  20.  
  21. # add game constraints
  22. game = filter(lambda x:x in '01.', game)
  23.  
  24. for ((r,c), val) in zip(vs, game):
  25. if val == '.': s.add(0 <= v[r][c], v[r][c] <= 1)
  26. else: s.add(v[r][c] == (int(val)))
  27.  
  28. # add board contraints
  29. def row(n): return [(n, i) for i in range(10)]
  30. def col(n): return [(i, n) for i in range(10)]
  31.  
  32. def row3(n,m): return [(n, i) for i in range(m,m+3)]
  33. def col3(n,m): return [(i, n) for i in range(m,m+3)]
  34.  
  35. for i in xrange(10):
  36. s.add(z3.Sum([v[r][c] for r,c in row(i)]) == 5)
  37. s.add(z3.Sum([v[r][c] for r,c in col(i)]) == 5)
  38.  
  39. for i in xrange(10):
  40. for j in xrange(8):
  41. s.add(z3.Sum([v[r][c] for r,c in row3(i,j)]) <= 2)
  42. s.add(z3.Sum([v[r][c] for r,c in row3(i,j)]) >= 1)
  43. s.add(z3.Sum([v[r][c] for r,c in col3(i,j)]) <= 2)
  44. s.add(z3.Sum([v[r][c] for r,c in col3(i,j)]) >= 1)
  45.  
  46. s.add(z3.Distinct([z3.Concat([v[r][c] for r,c in row(i)]) for i in xrange(10)]))
  47. s.add(z3.Distinct([z3.Concat([v[r][c] for r,c in col(i)]) for i in xrange(10)]))
  48.  
  49.  
  50. # find solution
  51. print s.check()
  52. m = s.model()
  53. sol = [[m[v[r][c]] for c in range(10)] for r in range(10)]
  54.  
  55. # print solution
  56. for r,c in vs:
  57. print str(sol[r][c]) + ("\n" if c==9 else ""),
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement