Bienvenu sur la page consacrée à au solveur LSAT.
Il a été par Bertrand MAZURE , Richard OSTROWSKI et
Lakhdar SAIS.
Ses principales caractéristiques sont:
- Recherche efficace des chaînes d'équivalences dans les CNF
- 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 par une autre ou clauses bloquées)
- Séparation des variables en deux ensembles (variables dépendantes/indépendantes) afin de brancher uniquement sur les variables indépendantes
- Heuristique classique: MOMS
La version 2.0 (sous licence CeCILL) est disponible ici (500k)
Quelques résultats lors de la dernière compétition SAT 2003
- Sur les instances industrielles
- Sur les instances "fait main"
