Essayez de le résoudre de différentes manières (SAT, CSP)

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éfinition des règles en mathématiques

Définissez une règle pour voir si votre programme a repris la définition

  1. Un numéro dans une cellule
  2. Un même numéro sur une ligne
  3. Un même numéro dans une colonne
  4. Un même numéro dans un bloc
  5. Satisfaire la contribution

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.

Définition

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).

Règle 1 (un nombre par carré)

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})

Règles 2,3,4 (un même nombre sur une ligne (colonne, bloc))

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.

Règle 5 (satisfaire l'entrée)

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.

la mise en oeuvre

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.

supposition

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.

Règles 2,3,4 (un même nombre sur une ligne (colonne, bloc))

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.

Règle 5 (satisfaire l'entrée)

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\}

la mise en oeuvre

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)
  ]

finalement

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

Essayez de le résoudre de différentes manières (SAT, CSP)
Diverses méthodes pour extraire les colonnes du tableau NumPy
Essayez de résoudre le Sudoku à une vitesse explosive en utilisant Numpy
Je veux résoudre SUDOKU
Différentes façons de calculer la similitude entre les données avec python
Essayez de calculer Trace en Python
Essayez de mettre des données dans MongoDB
6 façons d'enchaîner des objets en Python
Essayez Cython dans les plus brefs délais
Différentes façons de créer un tableau de nombres de 1 à 10 en Python.
Essayez de vous connecter à qiita avec Python
Essayez de reproduire l'add.at de NumPy avec Julia
J'ai essayé de laisser optuna résoudre le nombre
Je voulais résoudre ABC159 avec Python
Différentes façons de créer un dictionnaire (mémoires)
Divers commentaires à écrire dans le programme
Différentes façons de détruire des ressources avec une portée
Différentes façons de lire la dernière ligne d'un fichier csv en Python
Essayez d'afficher la séquence de Fibonacci dans différentes langues comme pratique d'algorithme
Essayez de résoudre le problème du fizzbuzz avec Keras
[Python] Compréhension de liste Différentes façons de créer une liste
Premiers pas pour essayer Google CloudVision en Python
Différentes façons d'exécuter des fichiers .py sous Windows
Essayez d'implémenter Oni Mai Tsuji Miserable avec python
3 façons d'analyser les chaînes de temps avec python [Note]
Calculons en fait le problème statistique avec Python
3.14 π jour, alors essayez de sortir en Python
Essayez auto pour évaluer automatiquement Enum dans Python 3.6
Essayez de résoudre le problème de l'héritage de classe Python
Essayez d'utiliser Blueprint avec Flask pour séparer les contrôleurs
Essayez de résoudre le diagramme homme-machine avec Python
Essayez de calculer RPN avec Python (pour les débutants)
Essayez d'imiter le paramètre _method de Rails dans webapp2
Notez que la méthode de publication des modules sur PyPI a changé de différentes manières.