Let's try solving Sudoku with various logic programming and see its advantages and disadvantages. I would like to introduce the following five
Define a rule to see if your program has taken over the definition
Suppose the input is represented by a tuple (x, y, i) that the condition "the value i is in the row x column y of the cell", and the entire input is represented by a list of that tuple.
SAT
** SAT Solver ** is an algorithm that finds whether there is a boolean value that satisfies a logical expression called CNF (Conjunctive Normal Form). CNF is represented by the logical product of a set of literal ORs (such as $ x_1 \ vee \ neg x_2 \ dots \ vee x_n $) called ** clauses **.
Now let's convert the rules to SAT.
Suppose $ g_ {x, y, i} $ is true when "the value i is in the row x column y of the cell". Conversely, $ g_ {x, y, i} $ is false when you say "the value i does not fit in the row x column y of the cell (other values fit)".
If you think about it easily, it looks like this
(g_{x,y,1} \wedge \neg g_{x,y,2} \wedge \dots \wedge\neg g_{x,y,9}) \vee(\neg g_{x,y,1} \wedge g_{x,y,2} \wedge \dots \wedge\neg g_{x,y,9}) \vee \dots \vee\\
(\neg g_{x,y,1} \wedge \neg g_{x,y,2} \wedge \dots\wedge g_{x,y,9})
But this is not a form of CNF, so if you expand it like the distributive law (?) And simplify it, it will be as follows.
(g_{x,y,1} \vee g_{x,y,2} \vee \dots g_{x,y,9}) \wedge (\neg g_{x,y,1} \vee \neg g_{x,y,2})\wedge (\neg g_{x,y,1} \vee \neg g_{x,y,3}) \wedge \dots \wedge\\
(\neg g_{x,y,8} \vee \neg g_{x,y,9})
The condition that "there is one or more numbers i in line x" can be written as follows:
g_{x,1,i} \vee g_{x,2,i} \vee \dots g_{x,9,i}
If you add the condition that "there are no more than two numbers i in line x" to this, it becomes rule 2, but if you combine it with rule 1, that condition becomes unnecessary. Because there is one or more numbers 1-9 in each of the 9 cells, [Pigeonhole Principle](https://ja.wikipedia.org/wiki/%E9%B3%A9%E3%81% AE% E5% B7% A3% E5% 8E% 9F% E7% 90% 86) Therefore, there can only be one number for each.
By the way, the condition that "there are no more than one number i in line x" is as follows.
(\neg g_{x,1,i} \vee \neg g_{x,2,i})\wedge (\neg g_{x,1,i} \vee \neg g_{x,3,i}) \wedge \dots \wedge(\neg g_{x,8,i} \vee \neg g_{x,9,i})
The same applies to columns and blocks, so they are omitted.
The condition that "the value i is in the row x column y of the cell" means that $ g_ {x, y, i} $ is assigned true.
So I will solve it using pysat's minisat.
from pysat.solvers import Minisat22
from itertools import product, combinations
def grid(i, j, k):
return i * 81 + j * 9 + k + 1
def sudoku_sat(arr):
m = Minisat22()
#Rule 1
for i, j in product(range(9), range(9)):
m.add_clause([grid(i, j, k) for k in range(9)])
for k1, k2 in combinations(range(9), 2):
m.add_clause([-grid(i, j, k1), -grid(i, j, k2)])
#Rule 2,3
for i in range(9):
for k in range(9):
m.add_clause([grid(i, j, k) for j in range(9)])
for j in range(9):
for k in range(9):
m.add_clause([grid(i, j, k) for i in range(9)])
#Rule 4
for p, q in product(range(3), range(3)):
for k in range(9):
m.add_clause([grid(i, j, k) for i, j in product(range(p*3, p*3+3), range(q*3, q*3+3))])
#Rule 5
for a in arr:
m.add_clause([grid(a[0], a[1], a[2] - 1)])
if not m.solve():
return None
model = m.get_model()
return [
[
[k + 1 for k in range(9) if model[grid(i, j, k) - 1] > 0][0]
for j in range(9)
]
for i in range(9)
]
CSP
~~ This is a copy / paste of university assignments ~~
** CSP (Constraint Programming) ** is an algorithm that solves the following $ V, D, C $ problems.
Suppose the variable $ v_ {x, y} $ is the value of the cell in row x column y. That is:
Rule 1 can be satisfied only with this premise.
If you write down the rule, it will be as follows
(v_{x,0}, v_{x,1})\in\{(1,2), (1,3), \dots (9,8)\} \\
(v_{x,0}, v_{x,2})\in\{(1,2), (1,3), \dots (9,8)\} \\
\vdots\\
(v_{x,7}, v_{x,8})\in\{(1,2), (1,3), \dots (9,8)\}
However, CSP usually has a convenient function called ʻAll Different`, which makes it easy to describe.
\text{AllDifferent}(v_{x,0}, v_{x,1},\dots,v_{x,8})
The same applies to columns and blocks.
Rule 5 can be incorporated from the domain, but it is represented by a constraint for the purpose of separating the input from the fundamental rule part of Sudoku. The constraint that "the value i is in the row x column y of the cell" is as follows
v_{x,y} \in \{i\}
Solve using python-constraint.
from constraint import Problem, AllDifferentConstraint, InSetConstraint
def sudoku_csp(arr):
def grid(i, j):
return '{}_{}'.format(i, j)
p = Problem()
for i, j in product(range(9), range(9)):
p.addVariable(grid(i, j), range(1, 10))
for i in range(9):
p.addConstraint(AllDifferentConstraint(), [grid(i, j) for j in range(9)])
p.addConstraint(AllDifferentConstraint(), [grid(j, i) for j in range(9)])
for m, n in product(range(3), range(3)):
p.addConstraint(
AllDifferentConstraint(),
[grid(i, j) for i, j in product(range(m*3, m*3+3), range(n*3, n*3+3))]
)
for a in arr:
p.addConstraint(InSetConstraint([a[2]]), [grid(a[0], a[1])])
solution = p.getSolution()
return [
[
solution[grid(i, j)]
for j in range(9)
]
for i in range(9)
]
If I do the Advent calendar in this condition, I'm going to die, so I'll cut corners next time.
Recommended Posts