ReViVal is a new preprocessing technique.

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.