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

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.