Codage SMT dans un espace de plans (liens causaux) pour la planification temporelle en temps continu

Frédéric Maris (1) , Maël Valais (1, 2) , Julien Vianey (1, 2)

1 IRIT-ADRIA - Argumentation, Décision, Raisonnement, Incertitude et Apprentissage
2 IRIT-LILaC - Logique, Interaction, Langue et Calcul

L'amélioration considérable des solveurs SAT a permis de les utiliser pour la résolution de divers problèmes d'intelligence artificielle, et en particulier la généra-tion automatique de plans d'actions. Récemment, des solveurs SMT (SAT Modulo Theory) prometteurs ba-sés sur des solveurs SAT efficaces ont été dévelop-pés. Il est donc intéressant d'utiliser le langage SMT qui nous permet de produire directement des codages de problèmes de planification temporelle sans avoir à discrétiser le temps ou à utiliser un gestionnaire de contraintes temporelles externe (Time Map Manager). Cette approche a déjà été explorée, mais la plupart des codages existants considèrent une modélisation dis-crète du temps. Nous introduisons dans cet article une nouvelle traduction de problèmes de planification tem-porelle en temps continu, basée sur un codage dans un espace de plans (liens causaux), en formules proposi-tionnelles modulo QF-RDL (Quantifier Free Rational Difference Logic).

Mots clés: temps; SAT; SMT; codages; Planification Automatique

Domaines: Intelligence artificielle [cs.AI]

Frédéric Maris, Maël Valais, Julien Vianey. Codage SMT dans un espace de plans (liens causaux) pour la planification temporelle en temps continu. Journées Francophones sur la Planification, la Décision et l'Apprentissage pour la conduite de systèmes (JFPDA @ PFIA 2018), LORIA : Laboratoire lorrain de Recherche en Informatique et ses Applications, France; AFIA : Association française pour l'intelligence artificielle, France, Jul 2018, Nancy, France. ⟨hal-01840825⟩