Lassen Sie uns versuchen, Supreme Germany mit verschiedenen logischen Programmen zu lösen und seine Vor- und Nachteile zu erkennen. Ich möchte die folgenden fünf vorstellen
Definieren Sie eine Regel, um festzustellen, ob Ihr Programm die Definition übernommen hat
Angenommen, die Eingabe wird durch ein Tapple "(x, y, i)" dargestellt, wobei die Bedingung "der Wert i befindet sich in der Zeile x Spalte y der Zelle", und die gesamte Eingabe wird durch eine Liste dieses Tapples dargestellt.
SAT
** SAT Solver ** ist ein Algorithmus, der ermittelt, ob es einen booleschen Wert gibt, der einem logischen Ausdruck namens CNF (Conjunctive Standard Form) entspricht. CNF wird durch das logische Produkt einer Reihe von Literalsummen (wie $ x_1 \ vee \ neg x_2 \ dots \ vee x_n $) dargestellt, die als ** Klauseln ** bezeichnet werden.
Lassen Sie uns nun die Regeln in SAT konvertieren.
Angenommen, $ g_ {x, y, i} $ ist wahr, wenn "Wert i in Zeile x Spalte y der Zelle steht". Umgekehrt ist $ g_ {x, y, i} $ falsch, wenn der Wert i nicht in die Zellenzeile x Spalte y passt (andere Werte passen).
Wenn Sie leicht darüber nachdenken, sieht es so aus
(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})
Dies erfolgt jedoch nicht in Form von CNF. Wenn Sie es also wie das Verteilungsgesetz (?) Erweitern und vereinfachen, wird es wie folgt aussehen.
(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})
Die Bedingung, dass "in Zeile x eine oder mehrere Zahlen i vorhanden sind", kann wie folgt geschrieben werden
g_{x,1,i} \vee g_{x,2,i} \vee \dots g_{x,9,i}
Wenn Sie die Bedingung hinzufügen, dass "in Zeile x nicht mehr als zwei Zahlen i vorhanden sind", wird dies zu Regel 2, aber wenn Sie sie mit Regel 1 kombinieren, wird diese Bedingung unnötig. Da es in jeder der neun Zellen eine oder mehrere Zahlen 1-9 gibt, [Dove Nest Principle](https://ja.wikipedia.org/wiki/%E9%B3%A9%E3%81% AE% E5% B7% A3% E5% 8E% 9F% E7% 90% 86) Daher kann jede Nummer nur einmal existieren.
Übrigens ist die Bedingung, dass "in Zeile x nicht mehr als eine Zahl i vorhanden ist", wie folgt.
(\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})
Gleiches gilt für Spalten und Blöcke, daher werden sie weggelassen.
Die Bedingung, dass "der Wert i in der Zeile x Spalte y der Zelle steht", bedeutet, dass $ g_ {x, y, i} $ true zugewiesen wird.
Also werde ich es mit Pysats Minisat lösen.
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()
#Regel 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)])
#Regel 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)])
#Regel 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))])
#Regel 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
~~ Dies ist eine Kopie einer Universitätsaufgabe ~~
** CSP (Constraint Programming) ** ist ein Algorithmus, der die folgenden $ V-, D-, C $ -Probleme löst.
Angenommen, die Variable $ v_ {x, y} $ ist der Wert der Zelle in Zeile x Spalte y. Das ist:
Regel 1 kann nur mit dieser Prämisse erfüllt werden.
Wenn Sie die Regel aufschreiben, lautet sie wie folgt
(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)\}
CSP verfügt jedoch normalerweise über eine praktische Funktion namens "AllDifferent", sodass Sie sie einfach beschreiben können, indem Sie sie verwenden.
\text{AllDifferent}(v_{x,0}, v_{x,1},\dots,v_{x,8})
Gleiches gilt für Spalten und Blöcke.
Regel 5 kann aus dem Definitionsbereich aufgenommen werden, wird jedoch durch eine Einschränkung dargestellt, um die Eingabe vom Grundregelteil der Zahl zu trennen. Die Einschränkung, dass "der Wert i in der Zeile x Spalte y der Zelle ist", ist wie folgt
v_{x,y} \in \{i\}
Lösen Sie mit 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)
]
Wenn ich den Adventskalender in diesem Zustand mache, werde ich sterben, also werde ich das nächste Mal Abstriche machen.
Recommended Posts