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.


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