Partenaires
Accueil du site > Logiciels > Prouveurs SAT
Prouveurs SAT
ReViVal
ReViVal est une technique de simplification (ou de vivification) de formules CNF développée par Cédric Piette, Youssef Hamadi et Lakhdar Saïs. La technique proposée exploite la déduction modulo la propagation unitaire pour la production de sous-clauses. Elle permet aussi d’utiliser différents schémas d’apprentissage pour produire de nouvelles clauses. La vivification peut être intégrée facilement dans un solveur SAT et tirer profit des récents (...)
ManySat
ManySat est un solveur parallèle de type DPLL incluant toute les fonctionnalités des solveurs SAT modernes (analyse de conflits, heuristique basée sur les activités, etc.) et celles issues de nos résultats récents sur l’amélioration des techniques d’analyse de conflits. Une description succinte du projet est disponible. Ce solveur est le fruit d’une collaboration entre Youssef Hamadi de Microsoft Cambridge (UK), Saïd Jabbour et Lakhdar Saïs du CRIL. Pour obtenir le logiciel (binaire uniquement), (...)
SAT4J : la bibliothèque SAT pour Java
SAT4J est une bibliothèque de prouveurs SAT en Java. Elle est conçue pour être facile à utiliser et performante sur les instances SAT issues de problèmes réels. La bibliothèque offre aussi la gestion des contraintes pseudo booléennes, et décline un grand nombre de problèmes de décision ou d’optimisation en terme de problème SAT ou pseudo booléen (MAXSAT, CSP). SAT4J est utilisée dans divers projets académiques : Alloy TASM AHEAD (...)
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,...). (...)