sift
Un solveur SAT (DPLL) avec une boite à outils de logique propositionnelle et un parseur DIMACS, en Haskell. Il résout de vraies instances et traduit les formules en CNF (Tseitin).
Un solveur SAT basé sur l'algorithme DPLL, écrit en Haskell, plus une boîte à outils de logique propositionnelle : un analyseur DIMACS et la traduction de formules en CNF par la méthode de Tseitin. Il résout de vraies instances.
Aperçu
sift est un solveur SAT basé sur l'algorithme DPLL, écrit en Haskell, accompagné d'une boîte à outils de logique propositionnelle : un analyseur du format DIMACS et la traduction de formules en forme CNF par la méthode de Tseitin. Ce n'est pas un exercice sur le papier - il résout de vraies instances.
SAT est l'un de ces problèmes qui allient une simplicité apparente à une profondeur énorme. La question paraît innocente, mais sa réponse peut trancher des problèmes de domaines tout à fait différents. Ce projet touche justement ce noyau, et sous un angle qui oblige à comprendre pourquoi un solveur fonctionne.
SAT pose une chose en apparence banale : peut-on choisir des valeurs de vérité pour que toute la formule soit vraie ? Banal jusqu'au moment où il y a des centaines de variables et où la réponse décide de la planification, de la vérification de circuits ou de la résolution d'un casse-tête. Un solveur SAT se trouve sous bien des problèmes difficiles que l'on traduit d'abord dans son langage.
L'entrée standard est le format DIMACS - chaque ligne est une clause, les nombres sont des variables, un moins est une négation, un zéro termine une clause. Du texte simple qui peut encoder des questions étonnamment difficiles.
Tseitin : pourquoi la CNF n'explose pas
DPLL exige une formule en CNF, mais toutes les formules ne le sont pas déjà. Une transformation naïve peut faire exploser sa taille de façon exponentielle, changeant un petit problème en un géant avant même le démarrage du solveur. La méthode de Tseitin introduit des variables auxiliaires et maintient une croissance linéaire.
Taille de la formule après conversion (à titre indicatif)
La méthode de Tseitin est l'une de ces astuces qui ressemblent à de la magie jusqu'à ce qu'on comprenne pourquoi elles marchent. Elle ajoute des variables auxiliaires qui en apparence compliquent la formule, mais qui en réalité sauvent sa taille - sans elles, une conversion naïve peut croître de façon exponentielle.
Le résultat : un solveur qui résout vraiment
Ce qui en sort est un solveur qui fonctionne, qui prend de vraies instances au format DIMACS et renvoie une réponse, et qui en chemin traduit n'importe quelle formule en CNF sans faire exploser sa taille. Écrit en Haskell, parce que le filtrage par motif et des types qui veillent à la justesse font que la logique se lit presque comme des mathématiques. Un petit projet qui touche une partie très profonde de l'informatique - et la résout vraiment.
Plus de projets
D'autres réalisations de la même catégorie - découvrez comment nous abordons des défis similaires.
Vous avez un projet similaire ?
Contactez-nous - le devis est gratuit et arrive sous une heure.
Comment fonctionne DPLL
DPLL est une recherche intelligente avec retour arrière. Au lieu d'essayer toutes les combinaisons, à chaque étape il choisit une variable, suppose sa valeur et surveille deux raccourcis : si une clause n'a qu'un seul littéral encore indécis, sa valeur est forcée ; si une variable apparaît toujours sous la même forme, on peut la fixer aussitôt.
Ce sont justement ces deux raccourcis qui font la différence entre une seconde et une éternité. Sans eux, le solveur erre dans l'arbre de toutes les possibilités ; avec eux, des sous-arbres entiers tombent avant même d'être visités. Les implémenter correctement est le cœur de tout le solveur.