Descriptif

L’objectif de cet enseignement est de présenter les algorithmes actuels de résolution (satisfiabilité ou non-satisfiabilité) de formules de logiques booléennes modélisant différents problèmes comme la planification de chemins, la planification de tâches, diagnostique. En particulier, l’algorithme DPLL, et son extension CDCL, seront présentés dans une première partie du cours pour résoudre des problèmes purement booléens. Ensuite, les extensions de formule de logiques avec des termes venant d’autres théories (expressions linéaires en nombres entiers, en nombres réels, ou expressions non-linéaires ou tableaux), qui sont à l’origine des techniques SMT (SAT Modulo Théories), seront présentées. Cette seconde partie permettra de faire le lien entre les algorithmes CDCL et les algorithmes classiques de programmation par contraintes ou de  programmation mathématique. Cet enseignement permettra de montrer comment des problèmes de décision complexes peuvent être résolus efficacement avec des techniques exploratoires.