123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117 |
- """
- The implementation of this Sudoku solver is based on the paper:
- "A SAT-based Sudoku solver" by Tjark Weber
- https://www.lri.fr/~conchon/mpri/weber.pdf
- If you want to understand the code below, in particular the function valid(),
- which calculates the 324 clauses corresponding to 9 cells, you are strongly
- encouraged to read the paper first. The paper is very short, but contains
- all necessary information.
- """
- import pycosat
- def v(i, j, d):
- """
- Return the number of the variable of cell i, j and digit d,
- which is an integer in the range of 1 to 729 (including).
- """
- return 81 * (i - 1) + 9 * (j - 1) + d
- def sudoku_clauses():
- """
- Create the (11745) Sudoku clauses, and return them as a list.
- Note that these clauses are *independent* of the particular
- Sudoku puzzle at hand.
- """
- res = []
- # for all cells, ensure that the each cell:
- for i in range(1, 10):
- for j in range(1, 10):
- # denotes (at least) one of the 9 digits (1 clause)
- res.append([v(i, j, d) for d in range(1, 10)])
- # does not denote two different digits at once (36 clauses)
- for d in range(1, 10):
- for dp in range(d + 1, 10):
- res.append([-v(i, j, d), -v(i, j, dp)])
- def valid(cells):
- # Append 324 clauses, corresponding to 9 cells, to the result.
- # The 9 cells are represented by a list tuples. The new clauses
- # ensure that the cells contain distinct values.
- for i, xi in enumerate(cells):
- for j, xj in enumerate(cells):
- if i < j:
- for d in range(1, 10):
- res.append([-v(xi[0], xi[1], d), -v(xj[0], xj[1], d)])
- # ensure rows and columns have distinct values
- for i in range(1, 10):
- valid([(i, j) for j in range(1, 10)])
- valid([(j, i) for j in range(1, 10)])
- # ensure 3x3 sub-grids "regions" have distinct values
- for i in 1, 4, 7:
- for j in 1, 4 ,7:
- valid([(i + k % 3, j + k // 3) for k in range(9)])
- assert len(res) == 81 * (1 + 36) + 27 * 324
- return res
- def solve(grid):
- """
- solve a Sudoku grid inplace
- """
- clauses = sudoku_clauses()
- for i in range(1, 10):
- for j in range(1, 10):
- d = grid[i - 1][j - 1]
- # For each digit already known, a clause (with one literal).
- # Note:
- # We could also remove all variables for the known cells
- # altogether (which would be more efficient). However, for
- # the sake of simplicity, we decided not to do that.
- if d:
- clauses.append([v(i, j, d)])
- # solve the SAT problem
- sol = set(pycosat.solve(clauses))
- def read_cell(i, j):
- # return the digit of cell i, j according to the solution
- for d in range(1, 10):
- if v(i, j, d) in sol:
- return d
- for i in range(1, 10):
- for j in range(1, 10):
- grid[i - 1][j - 1] = read_cell(i, j)
- def test():
- from pprint import pprint
- # hard Sudoku problem, see Fig. 3 in paper by Weber
- hard = [[0, 2, 0, 0, 0, 0, 0, 0, 0],
- [0, 0, 0, 6, 0, 0, 0, 0, 3],
- [0, 7, 4, 0, 8, 0, 0, 0, 0],
- [0, 0, 0, 0, 0, 3, 0, 0, 2],
- [0, 8, 0, 0, 4, 0, 0, 1, 0],
- [6, 0, 0, 5, 0, 0, 0, 0, 0],
- [0, 0, 0, 0, 1, 0, 7, 8, 0],
- [5, 0, 0, 0, 0, 9, 0, 0, 0],
- [0, 0, 0, 0, 0, 0, 0, 4, 0]]
- solve(hard)
- pprint(hard)
- assert [[1, 2, 6, 4, 3, 7, 9, 5, 8],
- [8, 9, 5, 6, 2, 1, 4, 7, 3],
- [3, 7, 4, 9, 8, 5, 1, 2, 6],
- [4, 5, 7, 1, 9, 3, 8, 6, 2],
- [9, 8, 3, 2, 4, 6, 5, 1, 7],
- [6, 1, 2, 5, 7, 8, 3, 9, 4],
- [2, 6, 9, 3, 1, 4, 7, 8, 5],
- [5, 4, 8, 7, 6, 9, 2, 3, 1],
- [7, 3, 1, 8, 5, 2, 6, 4, 9]] == hard
|