LSAT

LSAT : est un solveur SAT basé sur la procédure classique DPLL à laquelle a été ajouté un pré-traitement permettant de récupérer et d’exploiter les informations structurelles cachées par la forme normale conjonctive.

Ce solveur a été développé en C par Bertrand MAZURE , Richard OSTROWSKI et Lakhdar SAÏS. Il repose sur la procédure classique DPLL à laquelle ont été ajoutées les caractéristiques suivantes :

• Recherche efficace des chaînes d’équivalences
• Recherche syntaxique de certaines fonctions (et,ou,…). Une autre méthode basé sur la propagation unitaire plus efficace est en cours de réalisation
• Suppression de clauses « inutiles » (subsumées ou bloquées)
• Séparation des variables en deux ensembles (variables dépendantes/indépendantes) afin de brancher uniquement sur les variables indépendantes
• Heuristique de branchement classique : MOMS

LSAT a participé aux compétitions SAT en 2002 et 2003. En 2002, la version 1.0 de ce solveur était en démonstration. En 2003, LSAT (v2.0) a été primé : il a remporté la première phase de la compétition sur les instances « handmade » et a terminé deuxième lors de la phase finale. LSAT demeure le solveur ayant résolu le plus grand nombre d’instances de la catégorie « handmade ».

La version 2.0 (sous licence CeCILL) est disponible ici.