swMATH ID: 6958
Software Authors: Subbarayan, Sathiamoorthy; Pradhan, Dhiraj K.
Description: 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
Homepage: http://www.satisfiability.org/SAT04/programme/118.pdf
Related Software: MiniSat; Chaff; TPTP; Quantor; PicoSAT; z3; UBCSAT; Nenofex; sQueezeBF; BerkMin; StarExec; AVATAR; DISCOUNT; E Theorem Prover; FK-B; BooleForce; Lingeling; Coprocessor; DRAT-trim; CryptoMiniSat
Cited in: 20 Publications

Citations by Year