Descriptif

La logique formelle permet de représenter des connaissances mais également de raisonner sur ces connaissances pour en déduire de nouvelles informations. Dans cet enseignement, deux paradigmes de raisonnement seront étudiés afin de mettre en avant les modèles et algorithmes de résolution. Cet enseignement est divisé en deux parties: la première traitera des problèmes de satisfiabilité de formules de logiques booléennes (SAT) ainsi que leurs extension vers les problèmes de satisfiabilité modulo théories (SMT). La seconde partie abordera le domaine de la programmation par contraintes (CSP) qui permet de résoudre des problèmes combinatoires. Dans les deux parties, une séparation entre la partie modélisation à l'aide de formules booléennes ou de problèmes de satisfaction de contraintes et la partie résolution est réalisée. Cet enseignement permettra de montrer comment des problèmes de décision complexes peuvent être résolus efficacement avec des techniques exploratoires.