NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT Instances

S Subbarayan, DK Pradhan

Research output: Contribution to journalArticle (Academic Journal)peer-review

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 two 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. In the experiments, NiVER resulted in up to 74% decrease in N (Number of variables), 58% decrease in K (Number of clauses) and 46% decrease in L (Literal count). In many real-life instances, we observed that most of the resolvents for several variables are tautologies. Such variables are removed by NiVER. 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 insignificant. Empirical results using the state-of-the-art SAT solvers 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.
Translated title of the contributionNIVER: Non Increasing Variable Elimination Resolution for Preprocessing SAT Instances
Original languageEnglish
Article number276-291
Pages (from-to)276 - 291
Number of pages15
JournalLecture Notes in Computer Science (3542)
Volume3542
DOIs
Publication statusPublished - May 2004

Bibliographical note

ISBN: 3540278290
Publisher: Springer
Name and Venue of Conference: Theory and Applications of Satisfiability Testing: 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13
Other: http://www.cs.bris.ac.uk/Publications/pub_info.jsp?id=2000314
In Selected Revised Papers of International Conference on Theory and Applications of Satisfiability Testing Conference (Springer LNCS)

Fingerprint Dive into the research topics of 'NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT Instances'. Together they form a unique fingerprint.

Cite this