Essayons de résoudre Supreme Germany avec diverses programmations logiques et voyons ses avantages et ses inconvénients. Je voudrais vous présenter les cinq
Définissez une règle pour voir si votre programme a repris la définition
Supposons que l'entrée soit représentée par un tapple (x, y, i) que la condition "la valeur i est dans la ligne x colonne y de la cellule", et que l'entrée entière soit représentée par une liste de ce tapple.
SAT
** SAT Solver ** est un algorithme qui trouve s'il existe une valeur booléenne qui satisfait une expression logique appelée CNF (forme standard conjonctive). CNF est représenté par le produit logique d'un ensemble de sommes littérales (telles que $ x_1 \ vee \ neg x_2 \ dots \ vee x_n $) appelées ** clauses **.
Convertissons maintenant les règles en SAT.
Supposons que $ g_ {x, y, i} $ est vrai quand "la valeur i est dans la ligne x colonne y de la cellule". Inversement, $ g_ {x, y, i} $ est faux lorsque la valeur i ne rentre pas dans la ligne de cellule x colonne y (les autres valeurs correspondent).
Si tu y penses facilement, ça ressemble à ça
(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})
Mais ce n'est pas sous la forme de CNF, donc si vous le développez comme la loi de distribution (?) Et le simplifiez, ce sera comme suit.
(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})
La condition selon laquelle "il y a un ou plusieurs nombres i dans la ligne x" peut s'écrire comme suit
g_{x,1,i} \vee g_{x,2,i} \vee \dots g_{x,9,i}
Si vous ajoutez à cela la condition «il n'y a pas plus de deux nombres i dans la ligne x», cela devient la règle 2, mais si vous la combinez avec la règle 1, cette condition devient inutile. Comme il y a un ou plusieurs nombres 1 à 9 dans chacune des neuf cellules, [Principe du nid de colombe](https://ja.wikipedia.org/wiki/%E9%B3%A9%E3%81% AE% E5% B7% A3% E5% 8E% 9F% E7% 90% 86) Par conséquent, chaque numéro ne peut exister qu'une seule fois.
A propos, la condition selon laquelle "il n'y a pas plus d'un nombre i dans la ligne x" est la suivante.
(\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})
Il en va de même pour les colonnes et les blocs, ils sont donc omis.
La condition que "la valeur i est dans la ligne x colonne y de la cellule" signifie que $ g_ {x, y, i} $ est assigné vrai.
Je vais donc le résoudre en utilisant le minisat de pysat.
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()
#Règle 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)])
#Règle 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)])
#Règle 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))])
#Règle 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
~~ Ceci est une copie d'un devoir universitaire ~~
** CSP (Constraint Programming) ** est un algorithme qui résout les problèmes $ V, D, C $ suivants.
Supposons que la variable $ v_ {x, y} $ est la valeur de la cellule de la ligne x colonne y. C'est:
La règle 1 ne peut être satisfaite que par cette prémisse.
Si vous notez la règle, ce sera comme suit
(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)\}
Cependant, CSP a généralement une fonction pratique appelée «Tout différent», vous pouvez donc facilement le décrire en l'utilisant.
\text{AllDifferent}(v_{x,0}, v_{x,1},\dots,v_{x,8})
La même chose s'applique aux colonnes et aux blocs.
La règle 5 peut être incorporée à partir de la zone de définition, mais elle est représentée par une contrainte dans le but de séparer l'entrée de la partie de règle fondamentale du nombre. La contrainte selon laquelle "la valeur i est dans la ligne x colonne y de la cellule" est la suivante
v_{x,y} \in \{i\}
Résolvez en utilisant la contrainte python.
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)
]
Si je fais le calendrier de l'Avent dans ces conditions, je vais mourir, donc je vais couper les coins ronds la prochaine fois.
Recommended Posts