Résolution de contraintes qualitatives pour le temps et l'espace par SAT à partir de treillis

Session "Atelier RTE"National audienceDans cet article, nous proposons deux nouvelles traductions des réseaux de contraintes qualitatives (RCQ) pour le temps et l'espace en problème SAT. À partir d'un ordre partiel sur les relations de base formant un treillis, ces deux traductions SAT modélisent un découpage de chaque contrainte du RCQ considéré par des ensembles d'inter- valles du treillis et des propriétés reliant ces intervalles et les opérations de faible composition et d'inverse. Ces deux traductions peuvent être notamment utilisées dans le cadre du calcul des intervalles afin de traduire en problème SAT un RCQ à partir de l'ensemble des relations convexes