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 développements.