-
Notifications
You must be signed in to change notification settings - Fork 2
/
SudokuSolver.py
158 lines (116 loc) · 5.14 KB
/
SudokuSolver.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
from SudokuBoard import SudokuBoard
from Constants import ALEPH_NOUGHT
from yices import *
class SudokuSolver(object):
"""
The Sudoku Solver, will solve when asked.
iam: haven't really thought about the UI yet.
"""
def __init__(self, game):
self.game = game
# the matrix of uninterpreted terms
self.variables = self.__createVariables()
# the numerals as yices constants
self.numerals = self.__createNumerals()
# the yices configuration for puzzle solving
self.config = Config()
# is push and pop the default (yes; had to look at the source though.)
self.config.default_config_for_logic("QF_LIA")
# the context (a set/stack of yices assertions)
self.context = Context(self.config)
# add the generic constraints (corresponding to the rules of the game)
self.__generateConstraints()
# would take some (unnecessary) effort to hook these in somewhere
def __cleanUp(self):
self.context.dispose()
self.config.dispose()
Yices.exit()
def __createVariables(self):
"""Creates the matrix of uninterpreted terms that represents the logical view of the board."""
int_t = Types.int_type()
variables = SudokuBoard.newBoard()
for i in xrange(9):
for j in xrange(9):
variables[i][j] = Terms.new_uninterpreted_term(int_t)
return variables
def __createNumerals(self):
"""Creates a mapping from digits to yices constants for those digits."""
numerals = {}
for i in xrange(1, 10):
numerals[i] = Terms.integer(i)
return numerals
def __generateConstraints(self):
# each x is between 1 and 9
def between_1_and_9(x):
return Terms.yor([Terms.eq(x, self.numerals[i+1]) for i in xrange(9)])
for i in xrange(9):
for j in xrange(9):
self.context.assert_formula(between_1_and_9(self.variables[i][j]))
# All elements in a row must be distinct
for i in xrange(9):
self.context.assert_formula(Terms.distinct([self.variables[i][j] for j in xrange(9)]))
# All elements in a column must be distinct
for i in xrange(9):
self.context.assert_formula(Terms.distinct([self.variables[j][i] for j in xrange(9)]))
# All elements in each 3x3 square must be distinct
for k in xrange(3):
for l in xrange(3):
self.context.assert_formula(Terms.distinct([self.variables[i + 3 * l][j + 3 * k] for i in xrange(3) for j in xrange(3)]))
def __addFacts(self):
"""Adds the facts gleaned from the current state of the puzzle."""
def set_value(row, column, value):
assert 0 <= row and row < 9
assert 0 <= column and column < 9
assert 1 <= value and value <= 9
self.context.assert_formula(Terms.arith_eq_atom(self.variables[row][column], self.numerals[value]))
for i in xrange(9):
for j in xrange(9):
value = self.game.puzzle[i][j]
if value != 0:
set_value(i, j, value)
def solve(self):
"""Attempts to solve the puzzle, returning either None if there is no solution, or a board with the correct MISSING entries."""
solution = None
#we use push and pop so that we can solve (variants) repeatedly without having to start from scratch each time.
self.context.push()
self.__addFacts()
smt_stat = self.context.check_context(None)
if smt_stat != Status.SAT:
print 'No solution: smt_stat = {0}\n'.format(smt_stat)
else:
#get the model
model = Model.from_context(self.context, 1)
#return the model as a board with ONLY the newly found values inserted.
solution = SudokuBoard.newBoard()
for i in xrange(9):
for j in xrange(9):
if self.game.puzzle[i][j] == 0:
solution[i][j] = model.get_value(self.variables[i][j])
model.dispose()
self.context.pop()
return solution
#we could contrast the following with the yices_assert_blocking_clause
def countModels(self):
def model2term(model):
termlist = []
for i in xrange(9):
for j in xrange(9):
if self.game.puzzle[i][j] == 0:
val = model.get_value(self.variables[i][j])
var = self.variables[i][j]
value = self.numerals[val]
termlist.append(Terms.arith_eq_atom(var, value))
return Terms.yand(termlist)
result = 0
self.context.push()
self.__addFacts()
while self.context.check_context(None) == Status.SAT:
model = Model.from_context(self.context, 1)
diagram = model2term(model)
self.context.assert_formula(Terms.ynot(diagram))
model.dispose()
result += 1
if result == ALEPH_NOUGHT:
break
self.context.pop()
return result