Wednesday 26
Constraint programming and artificial intelligence
Simon de Givry
› 11:00 - 11:30 (30min)
› Bât A - TD 45
Un solveur hybride pour la résolution pratique de SAT
Jean-Marie Lagniez  1, *@  
1 : Centre de Recherche en Informatique de Lens  (CRIL)  -  Website
Université d'Artois, CNRS : UMR8188
Rue Jean Souvraz - SP 18 62307 LENS CEDEX -  France
* : Corresponding author

La programmation par contraintes est un paradigme de résolution très puissant, permettant de modéliser de nombreux problèmes dans différents domaines tels que les interfaces personne-machine, l'intelligence artificielle ou encore la recherche opérationnelle. Parmi ces langages de représentation, le langage des formules propositionnelles mises sous forme normale conjonctive (ou langage SAT) permet de modéliser et de résoudre de nombreux problèmes. Depuis l'avènement des solveurs CDCL (pour « Conflict Driven, Clause Learning »), le formalisme SAT est utilisé avec succès pour la résolution de problèmes applicatifs (vérification formelle bornée, gestion de dépendance, etc.). Ces méthodes sont effectivement très performantes sur les problèmes industriels, mais ne sont par exemple pas adaptées à la résolution de problèmes aléatoires, où les méthodes de recherche locales (RL) sont les plus efficaces. Une comparaison de ces deux paradigmes de recherche (CDCL et RL) montre que les avantages et les inconvénients de l'un correspondent respectivement aux inconvénients et aux avantages de l'autre, faisant de ces deux méthodes de potentiels partenaires complémentaires. Partant de ce constat, nous avons hybridé ces deux types d'approche afin d'en combiner les avantages. Nous étudierons et montrerons expérimentalement que notre approche est performante, en comparaison avec d'autre solveurs de l'état de l'art.


Online user: 1