Retour à l'index du GREYC

Séminaire Algorithmique

Site du CNRS

Séminaire Algorithmique

Le séminaire a lieu le mardi à 11 h 45 (sauf modification exceptionnelle), au campus Côte de Nacre, bâtiment Sciences 3, salle S3 351, 3ème étage.

Résumé du séminaire du Mardi 13 Février 2001

La Propagation de Contraintes et la Procedure DPLL pour le Raisonnement Propositionnel

par Min Li Chu (LaRIA, Universite de Picardie)

Nous presentons nos travaux de recherche dans la resolution pratique du probleme SAT et ses applications. Les resultats de cette recherche sont regroupes et justifies par la procedure DPLL (Davis-Putnam-Logemann-Loveland) appelee Satz et sa variation EqSatz qui permettent de resoudre de nombreux problemes SAT qui etaient hors de portee de l'etat de l'art.

La principale originalite de Satz est son heuristique de branchement basee sur la propagation des contraintes. Nous demontrons dans un premier temps sa puissance en la comparant aux autres methodes de la litterature sur differents problemes SAT. Puis nous suggerons que cette heuristique est probablement deja proche de l'optimale en effectuant une experimentation intensive. Une conclusion importante de cette etude est que l'on ne peut probablement plus ameliorer une procedure DPLL de facon substantielle par l'heuristique de branchement, et ce malgre les efforts intensifs des chercheurs dans cette direction.

Nous pensons qu'une procedure DPLL peut et doit encore etre amelioree par les regles de propagation de contraintes. Nous justifions cette idee en developpant EqSatz qui est Satz renforcee par la propagation des litteraux equivalents et qui est capable de resoudre une classe importante des problemes qui etaient hors de portee de la procedure DPLL. D'autres regles de propagations sont a etudier dans le futur.

GREYC
Campus Côte de Nacre, boulevard du Maréchal Juin
BP 5186
14032 Caen Cedex
FAX : +33 (0)2 31 56 73 30
http://www.greyc.fr