NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances The original algorithm for the SAT problem, Variable Elimination Resolution, has exponential space complexity. To tackle that, the backtracking-based DPLL procedure [{it M. Davis}, {it G. Logemann} and {it D. Loveland}, “A machine program for theorem-proving”, Commun. ACM 5, 394--397 (1962; Zbl 0217.54002)] 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.

References in zbMATH (referenced in 17 articles , 1 standard article )

Showing results 1 to 17 of 17.
Sorted by year (citations)

  1. Khasidashvili, Zurab; Korovin, Konstantin: Predicate elimination for preprocessing in first-order theorem proving (2016)
  2. KhudaBukhsh, Ashiqur R.; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin: SATenstein: automatically building local search SAT solvers from components (2016)
  3. Philipp, Tobias: An expressive model for instance decomposition based parallel SAT solvers (2015)
  4. Philipp, Tobias; Steinke, Peter: PBLib -- a library for encoding pseudo-Boolean constraints into CNF (2015)
  5. Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao: On QBF proofs and preprocessing (2013)
  6. Kullmann, Oliver; Zhao, Xishun: On Davis-Putnam reductions for minimally unsatisfiable clause-sets (2013)
  7. Järvisalo, Matti; Biere, Armin; Heule, Marijn J.H.: Simulating circuit-level simplifications on CNF (2012)
  8. Kupferschmid, Stefan; Lewis, Matthew; Schubert, Tobias; Becker, Bernd: Incremental preprocessing methods for use in BMC (2011)
  9. Giunchiglia, Enrico; Marin, Paolo; Narizzano, Massimo: sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning (2010)
  10. Heule, Marijn; Järvisalo, Matti; Biere, Armin: Clause elimination procedures for CNF formulas (2010)
  11. Pham, Duc Nghia; Thornton, John; Gretton, Charles; Sattar, Abdul: Combining adaptive and dynamic local search for satisfiability (2008)
  12. Condrat, Christopher; Kalla, Priyank: A Gröbner basis approach to CNF-formulae preprocessing (2007)
  13. Fourdrinoy, Olivier; Grégoire, Éric; Mazure, Bertrand; Saïs, Lakhdar: Eliminating redundant clauses in SAT instances (2007)
  14. Eén, Niklas; Biere, Armin: Effective preprocessing in SAT through variable and clause elimination (2005)
  15. Marinov, Darko; Khurshid, Sarfraz; Bugrara, Suhabe; Zhang, Lintao; Rinard, Martin: Optimizations for compiling declarative models into Boolean formulas (2005)
  16. Subbarayan, Sathiamoorthy; Pradhan, Dhiraj K.: NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances (2005)
  17. Zhang, Lintao: On subsumption removal and on-the-fly CNF simplification (2005)