Traduction logique et résolution de problèmes

Les solveurs pour les logiques classiques 

SAT : satisfaction de formules booléennes

 Le problème de satisfiabilité de formules booléennes (SAT) est connu comme étant le problème de référence pour la classe de complexité NP [Coo71]. Etant donné une formule propositionnelle en forme normale conjonctive (FNC), le problème SAT consiste à déterminer s’il existe un modèle de cette formule, c’est à dire une valuation pour chacune des variables de la formule qui rende vraie la formule. Par exemple, si nous prenons un ensemble de variables propositionnelles {a, b, c} et la formule Φ = (a ∨ b) ∧ (¬a ∨ b ∨ c) ∧ (¬a ∨ ¬b ∨ ¬c), nous pouvons remarquer que Φ est satisfiable. En effet, il suffit que les variables a et b aient la valeur vrai (>) et la variable c ait la valeur faux (⊥), ce qui nous donne un modèle de Φ. Il est possible, comme nous le verrons dans le chapitre 2, d’encoder de nombreux problèmes pour se ramener, pour les résoudre, à un problème de satisfiabilité de formule propositionnelle. 

SMT :SAT Modulo Theories 

Certains problèmes combinatoires nécessitent néanmoins de traiter des calculs sur les nombre naturels ou réels. Ceci peut être fait en utilisant seulement la logique propositionnelle (par exemple, 2 + 3 = 5 pourrait être codé par add2,3,5), mais c’est très inconfortable à moins qu’il n’y ait que quelques additions à faire. Ne parlons même pas des opérations de multiplication ou plus complexes. Le langage propositionnel de SAT a ainsi été étendu via SAT Modulo Theories (SMT) [NOT06]. Une instance SMT est composée d’une formule du premier ordre F qui peut  inclure des symboles de constantes, de prédicats et de fonctions, ainsi que d’une théorie T qui définit la sémantique des symboles. La question est : est-ce que F est satisfiable, sous réserve des interprétations des symboles imposées par T? Le langage SMT-LIB [BFT16] a été développé pour décrire des problèmes SMT. De nombreux solveurs existent aujourd’hui pour résoudre des problèmes pour différentes théories T comme la différence logique, l’arithmétique linéaire, les tableaux et les fonctions réelles non linéaires. Dans le cas de la combinaison du solveur SAT avec un solveur arithmétique, le but sera d’améliorer le traitement de la partie arithmétique du raisonnement. Dans de nombreux cas, ceci n’améliorera pas seulement l’efficacité du solveur, mais permettra aussi d’exprimer les contraintes arithmétiques des problèmes d’une manière radicalement plus compacte. Considérons le jeu de Kamaji 1 où le joueur doit grouper des nombres adjacents dans une grille de sorte que leur somme soit égale à un nombre fixe. Résoudre le jeu nécessite essentiellement un raisonnement logique mais a aussi besoin d’un peu d’arithmétique (addition). Si xi,j pour chaque case (i, j) est un entier et G(i, j, i, k) représente le fait que les cases (i, j) à (i, k) de la ligne i forment un groupe, la contrainte de somme pourrait être exprimée par : X m∈E xi,m = N où N est le nombre fixe et E est {j, j + 1, . . . , k}. La logique propositionnelle pure n’est certainement pas adaptée pour de telles phrases !

 QBF : formules booléennes quantifiées 

Quantified Boolean Formula (QBF) est connu comme étant le problème de référence pour la classe de complexité PSPACE ([SM73]). C’est une extension de la logique propositionnelle permettant de quantifier sur les variables propositionnelles. Par exemple, ∀p∃q.p ↔ q se lit : pour toute valeur de vérité de p, il existe une valeur de vérité de q tel que p ↔ q est vrai. Cette formule est vraie (il suffit de choisir la même valeur pour q que pour p). Alors que ∃p∀q.p ↔ q ne l’est pas. Ainsi, une formule booléenne quantifiée est toujours SOIT vraie SOIT fausse. De fait, à toute formule QBF peut être associée une formule propositionnelle sans variables car par définition : ∀p.Φ est vraie ssi Φ[p:=>] ∧ Φ[p:=⊥] l’est, et ∃p.Φ est vraie ssi Φ[p:=>] ∨ Φ[p:=⊥] est vraie. La formule QBF peut être exponentiellement plus compacte que la formule propositionnelle correspondante.

 La planification par compilation automatique

 En Intelligence Artificielle, la planification est un processus cognitif qui consiste à générer automatiquement, au travers d’une procédure formelle, un résultat articulé sous la forme d’un système de décision intégré appelé plan. Le plan est généralement sous la forme d’une collection organisée d’actions et il doit permettre à l’univers d’évoluer de l’état initial à un état qui satisfait le but. Dans le cadre classique, le plus restrictif, on considère les actions comme des transitions instantanées sans prendre en compte le temps. Dans le cadre temporel, on considère que les actions ont une durée d’exécution et que les événements associés aux actions ne sont plus instantanés mais peuvent avoir lieu à différents instants liés par des contraintes inhérentes aux actions. Une des approches algorithmiques pour la synthèse de plans est la compilation automatique (c’est-à-dire, la transformation) de problèmes de planification. Dans le planificateur SATPLAN [KS92], un problème de planification est compilé en une formule propositionnelle dont les modèles, correspondant aux plans-solutions, peuvent être trouvés en utilisant un solveur SAT. L’approche SAT recherche un plan solution de longueur fixe k. En cas d’échec cette longueur est augmentée avant de relancer la recherche d’une solution. Dans le cadre classique, décider s’il existe une solution est PSPACE-complet, mais la décision de l’existence d’une solution de taille polynomiale par rapport à la taille du problème est NPcomplete [Byl94]. Cette approche par compilation bénéficie directement des améliorations des solveurs SAT 2 . L’exemple le plus marquant est le planificateur BLACKBOX [KS98; KS99] (et ses successeurs SATPLAN’04 [Kau04] et SATPLAN’06 [KSH06]). Ces planificateurs ont obtenu la première place dans la catégorie planificateur optimal (en termes de nombre d’étapes du plan) des compétitions internationales de planification 3 IPC-2004 et IPC-2006. Ce résultat était inattendu car ces planificateurs étaient essentiellement des mises à jour de BLACKBOX et n’incluaient aucune réelle nouveauté : l’amélioration des performances était principalement due aux progrès du solveur SAT sous-jacent. De nombreuses améliorations de cette approche originale ont été proposées depuis lors, notamment via le développement de codages plus compacts et plus efficaces [KS96 ; EMW97; MK98; MK99; Rin03; RHN04; RHN06; Rin+08]. Suite à ces travaux, de nombreuses autres techniques similaires pour le codage de problèmes de planification ont été développées : Programmation Linéaire (LP) [WW99], Problèmes de Satisfaction de Contraintes (CSP) [DK01], SAT Modulo Theories (SMT) [SD05; MR08; Rina]. Plus récemment, une approche QBF (Quantified Boolean Formulas) a été proposée par [Rin07 ; CFG12] et nous avons proposé de nouveaux codages QBF dans [Gas+18].