NiVER: Non Increasing Variable Elimination Resolution for Preprocessing SAT instances

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 simplified 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 most of the cases, NiVER takes less than one second for preprocessing. In case NiVER removable variables are not present, due to very low overhead, the cost of NiVER is insignificant. We also study the effect of combining NiVER with HyPre [3], a preprocessor based on hyper binary resolution. Based on experimental results, we classify the SAT instances into 4 classes. NiVER consistently performs well in all those classes and hence can be incorporated into all general purpose SAT solvers.

Authors

• Sathiamoorthy Subbarayan
• Dhiraj K. Pradhan

Keywords

No keywords are indexed for this paper.