2014-03-28 Incremental SAT Solving

28 mars 2014, salle de Séminaires du Lirmm

Gilles Audemard,  Incremental SAT Solving

Les dernières avancées réalisées dans le cadre de la résolution
pratique du problème SAT ont rejailli bien au delà de ses frontières.
Ainsi, à l'heure actuelle, de nombreux problèmes dont la classe de
complexité est supérieure à NP peuvent être traités de manière pratique.
Pour la plupart, leur résolution consiste à appeler un solveur SAT sur
plusieurs instances analogues. Ce type de résolution, appelé résolution
incrémentale de SAT, est en passe de devenir l'état de l'art dans bien des
domaines.

Dans cet exposé nous commençons par rappeler les concepts basiques
des solveurs SAT actuels. Nous montrons ensuite le fonctionnement des solveurs SAT
incrémentaux à l'aide de deux applications : La recherche de noyaux minimalement
inconsistant et le requêtage d'une base de connaissance sans étape préalable de
compilation. A travers ces applications,  nous montrons également comment
améliorer glucose, un démonstrateur SAT état de l'art, pour le rendre
plus performant dans le cadre incremental.

Dernière mise à jour le 25/02/2015