Planification et résolution de problèmes SAT

En planification on s'intéresse à trouver des suites d'actions les plus courtes possibles qui permettent
d'atteindre un objectif donné partant d'un État initial donné (voir par exemple les tours de Hanoi, une action étant le déplacement d'un disque respectant la règle). Généralement on utilise en planification des systèmes dédiés. Une approche récente consiste à écrire les problèmes sous la forme de formules logiques du calcul propositionnel qui sont traitées à l'aide de solveurs SAT (Davis et Putnam, WSAT, satz,...). Pour ce travail il faudra :
  1. développer un solveur SAT
  2. écrire un traducteur de problèmes de planification plus ou moins général (dans un premier temps on pourra s'intéresser à des problèmes simples)
  3. valider l'approche expérimentalement.