Allow the possibility to compute counter models (negate a formula)
In some cases, it is necessary to compute counter examples of a formula (i;e. models of the negation of the formula).
It is easy to do that using the Plaisted-Greenbaum transformation, i.e. by adding a new fresh variable zi per constraint, creating binary clauses -zi \lor -lj for each clause, and adding a new clause containing all zi.
This could be performed easily in a decorator.