2 #Supervisor Dr. Konstantin Korovin
3 #http://pythonsudoku.sourceforge.net/
11 from os.path import basename
12 from itertools import combinations, ifilter, chain
13 from argprocessor import KSudokuArgParser
14 import csolversudoku as cs
16 argparser = KSudokuArgParser()
32 # note that the k is a number from 1 to 9
35 return (i * N**2 + j * N + k)
37 # note that the k is a number from 1 to 9
41 j = ((index -1)/ N) % N
43 return (i, j, k) # k is 1 - 9
46 def decode_to_matrix(result_list):
48 out_matrix = numpy.zeros(shape = (N,N))
50 if l > 0 and l < N**3+1:
51 #print l ,'means', (l-1)/81,((l-1)/9)%9,' is ', (l-1)%9 +1
59 def print_matrix(matrix):
69 def write_to_cnf_file(cnf, name): # out is the writting channel
70 out = open(name, 'w+')
73 for literal in clause:
74 out.write(str(literal)+' ')
79 def remove_cell_values(i, j, v):
80 if v in cellPossibleValues[i][j]:
81 cellPossibleValues[i][j].remove (v)
83 def add_cell_values(i, j, v):
84 if not (v in cellPossibleValues[i][j]):
85 cellPossibleValues[i][j].append(v)
87 def exactly_one(literals):
88 # print 'exactly one of ', literals
92 if len(literals) == 1:
93 cnf.append([literals[0]])
94 elif len(literals) == 2:
95 # cnf.append([literals[0], literals[1]])
96 cnf.append([literals[0] * -1, literals[1] * -1])
98 for x in literals[:-2]:
103 cnf.append([-1*x, -1*y])
104 # print 'x only one y'
106 # print 'link to the previous x and y'
107 cnf.append([x * -1, new[-1]])
108 # print [x * -1, new[-1]]
109 cnf.append([y * -1, new[-1]])
110 # print [y * -1, new[-1]]
113 # cnf.append([literals[-1], literals[-2]])
114 cnf.append([-1*literals[-1], -1*literals[-2]])
115 cnf.append([-1*literals[-1], new[-1]])
116 cnf.append([-1*literals[-2], new[-1]])
121 def encode_to_cnf(killerRules): #encode a problem (stored in matrix) as cnf
126 for i in range (0, N):
128 for j in range (0, N):
130 for num in range (1, N+1): # here, it represent num of 1 to 9
131 tmp2.append(getIndex(i, j, num))
133 indexBoard.append(tmp)
137 # find all possible combination of each cell
138 for k in killerRules:
142 cb = combinations([ii for ii in range(1, N+1)], cageSize)
143 f = lambda x : sum(x) == cageSum
144 comb = ifilter(f, cb) # all valid combinations
145 allPossible = list(chain(comb))
146 # print '\nall possible: ', allPossible
148 for i in range (1,N+1):
149 flag = True # means it is a common one
150 for j in allPossible:
151 # print 'test on', list(j)
152 if not(i in list(j)):
153 # print i, ' is not in ', list(j)
156 # print '************this is a common one: ', i
160 for p in allPossible:
168 # print 'In this iteration, we have the sum of cage: ', cageSum, '; the size of cage', cageSize
169 # print 'these cells are: ', cageCells
170 # print 'possible combinations are: ', allPossible
171 # print 'common values, ' , common
172 # print 'different values', different
174 # next we start to encode.
176 # encode the common values first.
177 # for every common value, [1,2] for example, introduce a new index representing the existence of the value
178 # among the cells of the cage.
181 for num in range(1, N+1):
182 dic[num] = getNewIndex()
185 cnf.append([indexBoard[cc[0]][cc[1]][num-1] * -1, dic[num]]) # right arrow
186 tmp.append(indexBoard[cc[0]][cc[1]][num-1]) # left arrow
187 tmp.append(dic[num] * -1)
190 # print num, ' is a common number'
191 cnf.append([dic[num]])
193 # next, we encode the differnt ones
194 # we need to introduce new values as above
195 # we need to obtain all the numbers possibly in the different cases
196 # lst = reduce ((lambda x, y: x + y), different)
197 # lst = list(set(lst)) # remove duplicated elements
200 for dif in different: # for example, [[3,4,8], [3,5,7], [4,5,6]
201 # for cc in cageCells:
202 # we need to convert from DNF to CNF
203 # first, we need to convert that x1 = 3 /\ 4 /\ 8
204 # again, we need to introduce our x1, for 348, x2 for 357 , etc
208 cnf.append([-1* x , dic[d]])
209 # print ' for ', d, ' -- ', dic[d]
211 # i.e. -3 \/ -4 \/ -8 \/ x
212 tmp = map ((lambda x : -1 * dic[x]), dif)
218 # print '***************', x_list
220 # END of killer sudoku ------------------------
221 countCNF_ari = len(cnf)
223 # Exactly one in each cell
224 for i in range(N): #column
225 for j in range(N): #row
226 # print 'for cell ', i ,' and ', j, '\n'
227 #at least one of k should be true
229 for k in range(1,N+1):
230 temp.append(getIndex(i,j,k))
231 cnf = cnf + exactly_one(temp)
233 #exactly once in each row
234 for k in range(1,N+1): #each number
235 # appear exactly once in each row
237 #appear at least once
238 #print 'In row ', j, ' \n'
241 temp.append(getIndex(i,j,k))
242 cnf = cnf + exactly_one(temp)
244 #exactly once in each coloumn
248 temp.append(getIndex(i,j,k))
249 cnf = cnf + exactly_one(temp)
250 #exactly once in each block
251 sqrRootN = int(N**(0.5))
252 for block_i in range(sqrRootN):
253 for block_j in range(sqrRootN):
254 #print 'for block', block_i, ' and ', block_j, '::::\n'
257 for i in range(block_i*sqrRootN, block_i*sqrRootN + sqrRootN):
258 for j in range(block_j*sqrRootN, block_j*sqrRootN + sqrRootN):
259 temp.append(getIndex(i,j,k))
260 cnf = cnf + exactly_one(temp)
261 countCNF_all = len(cnf)
265 def readSudoku(filename):
268 # print 'the constraints from file ', filename, ' are:'
269 name = re.findall("\d+", basename(filename[0]))
275 file_reader = open(filename[0], 'r')
276 lines = file_reader.readlines()
279 f = lambda x: [int(re.findall("(\d+)", x)[0]), int(re.findall("(\d+)", x)[1])]
283 (s, t) = l.split('=')
286 killerRules.append((int(s), lst))
289 def verify_killer_sudoku(killerRules, result_matrix):
290 # print 'start checking the answer!'
291 for r in killerRules:
296 cageSum = cageSum + result_matrix[c[0]][c[1]]
298 # print 'the rule is not validated: ', r
302 def solveOriginalEncoding(killerRules):
303 cnf = encode_to_cnf(killerRules)
304 # #solve the encoded CNF
306 result_list = pycosat.solve(cnf)
310 if result_list == 'UNSAT':
312 elif result_list !=[]:
313 print '*************\nTime in Sat Solver:\t%04.5f\ncountCNF_ari:\t%d\ncountCNF_ALL:\t%d\n'% ((end-start), countCNF_ari, countCNF_all)
314 return decode_to_matrix(result_list)
319 def solveKillerSudoku(killerRules):
324 if argparser.useCSolverEncoding() or argparser.shouldSerialize():
325 result_matrix = cs.solveProblem(N, killerRules, argparser.shouldSerialize())
327 result_matrix = solveOriginalEncoding(killerRules)
329 if result_matrix is None:
332 if (verify_killer_sudoku(killerRules, result_matrix)):
339 killerRules = readSudoku(argparser.getProblemName())
340 solveKillerSudoku(killerRules)
343 if __name__ == '__main__':