SAT 2004 START ConferenceManager    


NiVER: Non Increasing Variable Elimination Resolution for Preprocessing SAT instances

Sathiamoorthy Subbarayan and Dhiraj K Pradhan

Presented at The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004


Abstract

The original algorithm for SAT problem was VER due to Davis and Putnam. Unfortunately the algorithm results in memory explosion for most of the problem classes. To tackle with memory explosion, backtracking based DPLL procedure is used in modern SAT solvers. In this paper we present a combination of both the techniques. We use NiVER, a special case of VER, to eliminate some variables in a preprocessing step and then solve the simplified problem using a DPLL SAT solver. Most of the real-life instances have NiVER removable variables. We also study the effect of combining NiVER with HyPre preprocessor. NiVER is a simple approach, but it results in easier problem for several classes of SAT problems. In many cases, NiVER takes less than one second for preprocessing. In many cases around 50% of the variables are eliminated. NiVER adds very low overhead. NiVER shows good performance and hence deserves incorporation into all general-purpose SAT solvers.


  
START Conference Manager (V2.47.2)
Maintainer: rrgerber@softconf.com