ReVivAl : un nouveau préprocesseur pour SAT

Fruit d’une collaboration entre Youssef Hamadi, Lakhdar Saïs et Cédric Piette, ReVivAl (pour pReprocessing based on Vivification Algorithm) est une nouveau prétraitement pour formules CNF qui vise à produire des sous-clauses et générer de nouvelles clauses pertinentes.

Son efficacité est liée à sa complète intégration au sein d’un solver SAT.

Ainsi, il bénéficie des structures de données/mécanismes classiques des implémentations DPLL modernes (watched literals, apprentissage, heuristiques de type VSIDS, etc.), accélérant la production de (sous-)clauses.

Une page dédiée à ReVivAl est disponible ici (en anglais).