# NiVER: Non Increasing Variable Elimination Resolution

S. Subbarayan, Dhiraj Pradhan, NiVER: Non Increasing Variable Elimination Resolution. *Proceedings of The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT '04)*, pp. 351–356. May 2004. PDF, 179 Kbytes.
## Abstract

The original algorithm for the SAT problem, Variable Elimination
Resolution (VER/DP) has exponential space complexity. To tackle
that, the backtracking based DPLL procedure [2] is used in SAT solvers.
We present a combination of both of the techniques. We use NiVER, a
special case of VER, to eliminate some variables in a preprocessing step
and then solve the simpli_ed problem using a DPLL SAT solver. NiVER
is a strictly formula size not increasing resolution based preprocessor.
Best worst-case upper bounds for general SAT solving (arbitrary clause
length) in terms of N (Number of variables), K (Number of clauses)
and L (Literal count) are 2N, 20:30897K and 20:10299L, respectively [14].
In the experiments, NiVER resulted in upto 74% decrease in N, 58%
decrease in K and 46% decrease in L. In many real-life instances, we
observed that most of the resolvents for several variables are tautologies.
There will be no increase in space due to VER on them. Hence, despite
its simplicity, NiVER does result in easier instances. In case NiVER removable
variables are not present, due to very low overhead, the cost of
NiVER is insigni_cant. Empirical results show the usefulness of NiVER.
Some instances cannot be solved without NiVER preprocessing. NiVER
consistently performs well and hence can be incorporated into all general
purpose SAT solvers.

Bibtex entry.

## Contact details

## Publication Admin