NiVER 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 Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. Zbl 1122.68618Subbarayan, Sathiamoorthy; Pradhan, Dhiraj K. 2005 all top 5 Cited by 47 Authors 3 Biere, Armin 3 Heule, Marijn J. H. 2 Järvisalo, Matti 2 Philipp, Tobias 2 Zhang, Lintao 1 Becker, Bernd 1 Blanchette, Jasmin Christian 1 Bugrara, Suhabe 1 Condrat, Christopher 1 Darwiche, Adnan 1 Eén, Niklas 1 Fourdrinoy, Olivier 1 Gebser, Martin 1 Giunchiglia, Enrico 1 Grégoire, Éric 1 Gretton, Charles 1 Grigore, Radu 1 Hoos, Holger H. 1 Janhunen, Tomi 1 Janota, Mikoláš 1 Kalla, Priyank 1 Khasidashvili, Zurab O. 1 KhudaBukhsh, Ashiqur R. 1 Khurshid, Sarfraz 1 Korovin, Konstantin 1 Kullmann, Oliver 1 Kupferschmid, Stefan 1 Lewis, Matthew D. T. 1 Leyton-Brown, Kevin 1 Marin, Paolo 1 Marinov, Darko 1 Marques-Silva, João P. 1 Marquis, Pierre 1 Mazure, Bertrand 1 Narizzano, Massimo 1 Pham, Duc Nghia 1 Pradhan, Dhiraj K. 1 Rinard, Martin C. 1 Rintanen, Jussi 1 Saïs, Lakhdar 1 Sattar, Abdul 1 Schubert, Tobias 1 Steinke, Peter 1 Subbarayan, Sathiamoorthy 1 Vukmirović, Petar 1 Xu, Lin 1 Zhao, Xishun all top 5 Cited in 7 Serials 1 Artificial Intelligence 1 Theoretical Computer Science 1 Journal of Automated Reasoning 1 Formal Methods in System Design 1 The Journal of Artificial Intelligence Research (JAIR) 1 ACM Transactions on Computational Logic 1 Journal of Satisfiability, Boolean Modeling and Computation Cited in 3 Fields 19 Computer science (68-XX) 3 Mathematical logic and foundations (03-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year