N-Reines avec un solveur SAT¶

2024 Résolution de problèmes

Le problème des N-reines consiste en un échiquier possédant n cases de côté, sur lequel sont placées n reines de telle sorte qu’aucune ne soit en prise avec une autre.

Introduction¶

Pour résoudre ce problème, nous devons considérer deux caractéristiques principales : le codage de la solution et les contraintes. Le codage de la solution, ou représentation de la solution, a un impact significatif sur l’architecture de l’algorithme et sur sa performance. Le codage de la solution est un vecteur à une dimension dont l’indice correspond à la colonne et la valeur de la case correspond à la ligne. Il y a quatre contraintes : ligne, colonne, diagonale et anti-diagonale. Et pour limiter le nombre de solutions valides, nous devons identifier les types de symétrie, comme la symétrie axiale et centrale. Et donc ajouter des contraintes pour briser la symétrie. Ce problème est utilisé pour introduire l’algorithme de backtracking. Mais de nombreuses façons sont possibles pour résoudre ce problème. Nous pouvons utiliser un solveur utilisant des techniques de programmation par contraintes (PPC) comme or-tool, choco ou gecode. Ou traduire le problème des N-reines en un problème SAT et utiliser un solveur SAT (comme PicoSAT).

Backtracking¶

L’espace des solutions est exploré à l’aide d’un arbre, chaque nœud correspond à une sous-solution ou une solution, et la feuille à une solution valide. L’algorithme 1 décrit un backtracking récursif. L’exploration de l’arbre est effectuée par un parcours en profondeur (depth-first search) et, pour chaque sous-solution visitée, un filtrage est appliqué afin de déterminer s’il s’agit d’une solution valide ou non.

S’il s’agit d’une solution valide, ses enfants sont visités à leur tour. Le filtrage utilise les propriétés du problème pour couper les branches les moins intéressantes le plus tôt possible. Il n’est pas nécessaire d’avoir la contrainte de colonne, car la propriété du codage de la solution fixe cette contrainte au préalable.

Soit un vecteur \(V\) de taille \(n\), unidimensionnel, représentant la position des reines sur un échiquier, avec

\[V = \{v_0, v_1, ..., v_n\}\]

La contrainte de ligne peut être formalisée

\[\forall i, j \in n, v_{i} \neq v_{j} | i \neq j\]

Algorithme 1 (Backtracking)

Backtrack(s, depth, \(s^{*}\))

si \(|s|\) == depth alors \(s \leftarrow s^{*} \cup s\)
pour chaque i dans range(N)
- \(s^{\prime} \leftarrow s + [i]\)
- vérifier les contraintes sur \(s^{\prime}\) : ligne, diagonale, anti-diagonale
- si aucune contrainte n’est violée alors
  - Backtrack(\(s^{\prime}\), depth + 1, \(s^{*}\))

Solveur SAT¶

Le problème de satisfiabilité booléenne (SAT) consiste, étant donné une formule booléenne, à déterminer s’il existe une façon d’assigner des valeurs aux variables telle que, s’il est possible de satisfaire cette formule, celle-ci devienne entièrement vraie. Réduire le problème des N-reines au problème SAT, tout en conservant autant que possible les propriétés du problème original, permet (i) d’étudier le problème et (ii) d’utiliser un solveur efficace sans développer un nouveau solveur ad hoc pour un problème spécifique. Dans notre cas, nous devons convertir chaque propriété du problème des N-reines en clauses sous forme normale conjonctive (CNF). Un exemple de CNF :

\[ (A \lor B ) \land ( \neg C \lor \neg D) \]

Nous devons définir les clauses pour chaque variable impliquée dans les contraintes du problème. Notez que le nombre de variables est exponentiel en fonction de \(N\), car nous avons besoin d’une variable pour chaque case de l’échiquier.

Définition des clauses CNF¶

La définition des contraintes s’effectue en donnant la relation entre chaque variable et les autres variables liées. Prenons un exemple avec 4-Reines et 16 variables, chaque variable correspondant à une case de l’échiquier.

Contrainte de ligne (pour la première ligne)

\[\begin{split}\begin{align*} & (V_1 \lor V_2 \lor V_3 \lor V_4) \\ \land & (\neg V_1 \lor \neg V_2) \\ \land & (\neg V_1 \lor \neg V_3) \\ \land & (\neg V_1 \lor \neg V_4) \\ \land & (\neg V_2 \lor \neg V_3) \\ \land & (\neg V_2 \lor \neg V_4) \\ \land & (\neg V_3 \lor \neg V_4) \end{align*}\end{split}\]

Contrainte de colonne (pour la première colonne)

\[\begin{split}\begin{align*} & (V_{1} \lor V_{5} \lor {9} \lor V_{13}) \\ \land & (\neg V_{1} \lor \neg V_{5}) \\ \land & (\neg V_{1} \lor \neg V_{9}) \\ \land & (\neg V_{1} \lor \neg V_{13}) \\ \land & (\neg V_{5} \lor \neg V_9) \\ \land & (\neg V_{5} \lor \neg V_{13}) \\ \land & (\neg V_{9} \lor \neg {V_13}) \end{align*}\end{split}\]

Diagonale

\[\begin{split}\begin{align*} & V_{2} \lor \neg V_{7} \lor \neg V_{12} \\ \land & (\neg V_{2} \neg V_{7}) \\ \land & (\neg V_{2} \neg V_{12}) \\ \land & (\neg V_{7} \neg V_{12}) \end{align*}\end{split}\]

Format DIMACS CNF¶

Le format DIMACS CNF pris en charge par PicoSAT est organisé de la manière suivante : (i) chaque ligne commençant par \(c\) est un commentaire, (ii) chaque ligne commençant par \(p\) décrit la section des clauses avec le nombre de variables et le nombre de clauses, et pour chaque ligne de clause, la fin de ligne contient \(0\).

Exemple d’un format DIMACS CNF :

c Here is a comment.
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

En clause CNF :

\[\begin{split}\begin{align*} & (V_{1} \lor \neg V_{5} \lor V_{4}) \\ \land & (\neg V_{1} \lor V_{5} \lor V_{3} \lor V_{4}) \\ \land & (\neg V_{3} \lor \neg V_{4}) \end{align*}\end{split}\]

Pour chaque instance du problème des N-reines, nous devons définir toutes les clauses. Pour cela, nous devons écrire un générateur.

Comment utiliser le solveur¶

Installer le solveur SAT, disponible dans les dépôts sous Ubuntu

sudo apt install picosat

Pour exécuter le solveur avec le chemin du fichier DIMACS en paramètre. Le solveur retourne toutes les valeurs booléennes pour chaque variable ; les variables négatives représentent Faux et les variables positives représentent Vrai.

$ picosat 4-queens.cnf
s SATISFIABLE
v -1 -2 3 -4 5 -6 -7 -8 -9 -10 -11 12 -13 14 -15 -16 0

Expériences¶

L’expérience est réalisée avec le générateur de clauses CNF pour le problème des N-reines, écrit en CPP et disponible ici. Pour réaliser l’expérimentation, nous utilisons une machine Linux avec 8 Go et un i7-4790K à 4GHz.

Tableau 1 Résoudre le problème des N-reines avec un solveur SAT¶
N	# Clauses	Temps de résolution (s)
100	1 647 290	0.653
200	13 254 590	11.481
300	44 821 890	21.054
400	106 349 190	51.301
500	207 836 490	241.55

Le tableau 1 décrit le nombre de clauses et le temps de résolution du solveur PicoSAT pour chaque instance de taille N.

Conclusion¶

Résoudre le problème des N-reines à l’aide d’un problème SAT s’effectue en traduisant les propriétés du problème original dans ce nouveau problème, tout en conservant les propriétés du problème d’origine. Mais en pratique, le solveur SAT n’est pas la bonne approche pour ce problème, car le nombre de variables augmente de manière exponentielle en fonction de la taille de l’échiquier. Cependant, l’algorithme de backtracking sera plus efficace, grâce à un nombre de variables limité et à une coupe efficace des branches le plus tôt possible.