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 :
-
développer un solveur SAT
-
é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)
-
valider l'approche expérimentalement.