Modélisation SAT

Cours

1. Le problème SAT, Wikipedia Fr et En
2. L'algorithme DPLL pour résoudre SAT
3. Un premier exemple de modélisation SAT : le problème du pigeonnier (pour en savoir plus : le principe des tiroirs).
   Remarque : outre l'intérêt pédagogique de la modélisation SAT du problème du pigeonnier, son intérêt pratique est de pousser les solveurs SAT basés sur DPLL (qui sont actuellement les plus efficaces en général) dans leurs derniers retranchements.
   1. Tutoriel sur les solveurs SAT et le format DIMACS
   2. Quelques modèles Dimacs à tester avec un solveur SAT :
      • MiniSAT
      • MiniSAT version Javascript utilisable sur un navigateur
      • SAT4J, un solveur SAT en Java
   3. Ecrire un programme (Python, Shell, Java ou autre) qui génère le fichier DIMACS correspondant au problème P(m,n)
   4. Constater que trouver une solution pour P(m,m) est rapide même pour des valeurs de m élevées alors que montrer qu'il n'y a pas de solution pour P(m+1,m) est exponentiel en m.

Exercices

1. Coloriage de cartes : intro, modélisation
2. Les 8 reines
3. Le Sudoku
4. La planification