Loveland, Donald; Sabharwal, Ashish; Selman, Bart DPLL: the core of modern satisfiability solvers. (English) Zbl 1439.68026 Omodeo, Eugenio G. (ed.) et al., Martin Davis on computability, computational logic, and mathematical foundations. Cham: Springer. Outst. Contrib. Log. 10, 315-335 (2016). MSC: 68V15 68-03 68R07 68T20 PDF BibTeX XML Cite \textit{D. Loveland} et al., Outst. Contrib. Log. 10, 315--335 (2016; Zbl 1439.68026) Full Text: DOI
Marić, Filip Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. (English) Zbl 1208.68205 Theor. Comput. Sci. 411, No. 50, 4333-4356 (2010). MSC: 68T20 68Q60 PDF BibTeX XML Cite \textit{F. Marić}, Theor. Comput. Sci. 411, No. 50, 4333--4356 (2010; Zbl 1208.68205) Full Text: DOI
Marić, Filip; Janičić, Predrag Formal correctness proof for DPLL procedure. (English) Zbl 1209.68514 Informatica, Vilnius 21, No. 1, 57-78 (2010). MSC: 68T20 PDF BibTeX XML Cite \textit{F. Marić} and \textit{P. Janičić}, Informatica, Vilnius 21, No. 1, 57--78 (2010; Zbl 1209.68514) Full Text: Link
Wernhard, Christoph Automated deduction for projection elimination. (English) Zbl 1200.68227 DISKI. Dissertationen zur Künstlichen Intelligenz 324. Heidelberg: Akademische Verlagsgesellschaft Aka; Amsterdam: IOS Press (Diss. 2008) (ISBN 978-1-58603-983-7; 978-3-89838-324-0/pbk). x, 273 p. (2009). Reviewer: Ion Iancu (Craiova) MSC: 68T30 68T15 68T27 68-02 PDF BibTeX XML Cite \textit{C. Wernhard}, Automated deduction for projection elimination. Heidelberg: Akademische Verlagsgesellschaft Aka; Amsterdam: IOS Press (Diss. 2008) (2009; Zbl 1200.68227)
Tveretina, Olga; Wesselink, Wieger EufDPLL – a tool to check satisfiability of equality logic formulas. (English) Zbl 1336.68167 Seda, Anthony (ed.) et al., Proceedings of the Irish conference on the mathematical foundations of computer science and information technology (MFCSIT 2006), National University of Ireland, Cork, Ireland, August 1–5, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 225, 405-420 (2009). MSC: 68Q60 03B70 68T15 PDF BibTeX XML Cite \textit{O. Tveretina} and \textit{W. Wesselink}, Electron. Notes Theor. Comput. Sci. 225, 405--420 (2008; Zbl 1336.68167) Full Text: DOI
Baumgartner, Peter; Tinelli, Cesare The model evolution calculus as a first-order DPLL method. (English) Zbl 1182.03034 Artif. Intell. 172, No. 4-5, 591-632 (2008). MSC: 03B35 68T15 68T20 PDF BibTeX XML Cite \textit{P. Baumgartner} and \textit{C. Tinelli}, Artif. Intell. 172, No. 4--5, 591--632 (2008; Zbl 1182.03034) Full Text: DOI
Sinz, Carsten Visualizing SAT instances and runs of the DPLL algorithm. (English) Zbl 1129.68502 J. Autom. Reasoning 39, No. 2, 219-243 (2007). MSC: 68T15 68T20 PDF BibTeX XML Cite \textit{C. Sinz}, J. Autom. Reasoning 39, No. 2, 219--243 (2007; Zbl 1129.68502) Full Text: DOI
Badban, Bahareh; Van De Pol, Jaco; Tveretina, Olga; Zantema, Hans Generalizing DPLL and satisfiability for equalities. (English) Zbl 1121.68102 Inf. Comput. 205, No. 8, 1188-1211 (2007). MSC: 68T15 68T20 03B25 03B35 PDF BibTeX XML Cite \textit{B. Badban} et al., Inf. Comput. 205, No. 8, 1188--1211 (2007; Zbl 1121.68102) Full Text: DOI
Tveretina, Olga A decision procedure for equality logic with uninterpreted functions. (English) Zbl 1109.68581 Buchberger, Bruno (ed.) et al., Artificial intelligence and symbolic computation. 7th international conference, AISC 2004, Linz, Austria, September 22–24, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23212-5/pbk). Lecture Notes in Computer Science 3249. Lecture Notes in Artificial Intelligence, 66-79 (2004). MSC: 68T15 68T20 PDF BibTeX XML Cite \textit{O. Tveretina}, Lect. Notes Comput. Sci. 3249, 66--79 (2004; Zbl 1109.68581) Full Text: DOI
Lagoudakis, Michail G.; Littman, Michael L. Learning to select branching rules in the DPLL procedure for satisfiability. (English) Zbl 0990.90543 Kautz, Henry (ed.) et al., LICS 2001 workshop on theory and application of satisfiability testing (SAT 2001). Boston, MA, USA, June 14-15, 2001. Amsterdam: Elsevier, Electron. Notes Discrete Math. 9, no pag., electronic only (2001). MSC: 90C27 PDF BibTeX XML Cite \textit{M. G. Lagoudakis} and \textit{M. L. Littman}, Electron. Notes Discrete Math. 9, no pag. (2001; Zbl 0990.90543)
Bailey, Delbert D.; Dalmau, Victor; Kolaitis, Phokion G. Phase transitions of PP-complete satisfiability problems. (Abstract). (English) Zbl 0990.90547 Kautz, Henry (ed.) et al., LICS 2001 workshop on theory and application of satisfiability testing (SAT 2001). Boston, MA, USA, June 14-15, 2001. Amsterdam: Elsevier, Electron. Notes Discrete Math. 9, no pag., electronic only (2001). MSC: 90C27 90C60 PDF BibTeX XML Cite \textit{D. D. Bailey} et al., Electron. Notes Discrete Math. 9, no pag. (2001; Zbl 0990.90547)