Description
ReViVal is a new preprocessing technique developped by Cédric Piette, Youssef Hamadi and Lakhdar Saïs.
The main idea is to perform particular forms of resolution (through Unit Propagation) for efficiently producing sub-clauses. It can also use different schemes of learning to add relevant clauses. The vivification algorithm ReViVal is based on is designed to be fully integrated within a SAT solver, taking advantage of most recent techniques and data structures implemented for SAT. A version based on Minisat 1.14 is available below, but the vivification procedure described here can be easily grafted to most of SAT solvers.
Ressources
Different combinations of ReVivAl and SatElite have been submitted to the preprocessor track of the SAT competition 2009. In the final results, the submitted procedure came in 2nd for both APPLICATION and CRAFTED categories (and 1st in the UNSAT CRAFTED category).
Source code of version v0.23 This new version fixes some bugs and improves the average behavior of the procedure. New features (no learning, randomized seed, verbose mode, etc.) are available by manipulating the flags in the source code (see main.c file for options to (un)activate)
ReVivAl 0.23 evaluation page The new version of ReVivAl has been extensively evaluated. The behavior of minisat 2.0 with or without the use of ReVivAl have been compared on a large number of instances. Synthesis and detailled results are available here.
A special thank to Olivier Roussel for making his evaluation system available.
Source code of version v0.16 First release. Mainly a cleaned-up version of 0.14.
"Vivifying Propositionnal Clausal Formulae" Cédric Piette, Youssef Hamadi and Lakhdar Saïs, ECAI'08 paper
Extensive Experimental Results: The ECAI'08 Paper provides with a representative sample of obtained experimental results, but an extended version (which presents comparison of SatElite and ReVivAl on thousands of instances) is available here. This comparison has been done with version 0.14 of ReVivAl. With new versions, even better results could be expected.
Binairies of version v0.14, which has participated to the SAT-Race'08 through the solver preSAT (6th on 19 submitted solvers).
Links
Back to Cédric Piette Home Page
Lens Computer Science Research Centre (CRIL) where I am working.