DPLL(T)

{{Short description|Algorithm to solve SMT problems}}

In computer science, DPLL(T) is a framework for determining the satisfiability of SMT problems. The algorithm extends the original SAT-solving DPLL algorithm with the ability to reason about an arbitrary theory T.{{Cite book|last1=Ganzinger|first1=Harald|last2=Hagen|first2=George|last3=Nieuwenhuis|first3=Robert|last4=Oliveras|first4=Albert|last5=Tinelli|first5=Cesare|date=2004|editor-last=Alur|editor-first=Rajeev|editor2-last=Peled|editor2-first=Doron A.|chapter=DPLL(T): Fast Decision Procedures|title=Computer Aided Verification|volume=3114|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=175–188|doi=10.1007/978-3-540-27813-9_14|isbn=9783540278139|doi-access=free}}{{Cite journal|last1=Nieuwenhuis|first1=Robert|last2=Oliveras|first2=Albert|last3=Tinelli|first3=Cesare|date=2006|title=Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T)|journal=J. ACM|volume=53|issue=6|pages=937–977|doi=10.1145/1217856.1217859|s2cid=14058631 |issn=0004-5411}}{{Cite book|last1=Nieuwenhuis|first1=Robert|last2=Oliveras|first2=Albert|date=2005|editor-last=Etessami|editor-first=Kousha|editor2-last=Rajamani|editor2-first=Sriram K.|chapter=DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic|title=Computer Aided Verification|volume=3576|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=321–334|doi=10.1007/11513988_33|isbn=9783540316862|doi-access=free}} At a high level, the algorithm works by transforming an SMT problem into a SAT formula where atoms are replaced with Boolean variables. The algorithm repeatedly finds a satisfying valuation for the SAT problem, consults a theory solver to check consistency under the domain-specific theory, and then (if a contradiction is found) refines the SAT formula with this information.{{Cite web|url=http://homepage.divms.uiowa.edu/~ajreynol/pres-dpllt15.pdf|title=Satisfiability Modulo Theories and DPLL(T)|last=Reynolds|first=Andrew|date=2015|website=The University of Iowa|archive-url=|archive-date=|access-date=2019-04-08}}

Many modern SMT solvers, such as Microsoft's Z3 Theorem Prover and CVC4, use DPLL(T) to power their core solving capabilities.{{Cite book|last1=de Moura|first1=Leonardo|last2=Bjørner|first2=Nikolaj|date=2008|editor-last=Ramakrishnan|editor-first=C. R.|editor2-last=Rehof|editor2-first=Jakob|chapter=Z3: An Efficient SMT Solver|title=Tools and Algorithms for the Construction and Analysis of Systems|volume=4963|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=337–340|doi=10.1007/978-3-540-78800-3_24|isbn=9783540788003|doi-access=free}}{{Cite book |last1=Liang |first1=Tianyi |last2=Reynolds |first2=Andrew |last3=Tinelli |first3=Cesare |last4=Barrett |first4=Clark |last5=Deters |first5=Morgan |date=2014 |editor-last=Biere |editor-first=Armin |editor2-last=Bloem |editor2-first=Roderick |chapter=A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions |title=Computer Aided Verification |series=Lecture Notes in Computer Science |language=en |location=Cham |publisher=Springer International Publishing |pages=646–662 |doi=10.1007/978-3-319-08867-9_43 |isbn=978-3-319-08867-9|doi-access=free }}{{Cite book|last1=Bruttomesso|first1=Roberto|last2=Cimatti|first2=Alessandro|last3=Franzén|first3=Anders|last4=Griggio|first4=Alberto|last5=Sebastiani|first5=Roberto|date=2008|editor-last=Gupta|editor-first=Aarti|editor1-link=Aarti Gupta (computer scientist)|editor2-last=Malik|editor2-first=Sharad|chapter=The MathSAT 4 SMT Solver|title=Computer Aided Verification|volume=5123|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=299–303|doi=10.1007/978-3-540-70545-1_28|isbn=9783540705451|doi-access=free}}