DPLL(T)

DPLL(T)

DPLL(T)

Add article description

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.[1][2][3] 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.[4]

Many modern SMT solvers, such as Microsoft's Z3 Theorem Prover and CVC4, use DPLL(T) to power their core solving capabilities.[5][6][7]

References

  1. [1]
    Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2004). Alur, Rajeev; Peled, Doron A. (eds.). DPLL(T): Fast Decision Procedures. Lecture Notes in Computer Science. Vol. 3114. Springer Berlin Heidelberg. pp. 175–188. doi:10.1007/978-3-540-27813-9_14. ISBN 9783540278139. {{cite book}}: |journal= ignored (help)
  2. [2]
    Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2006). "Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T)". J. ACM. 53 (6): 937–977. doi:10.1145/1217856.1217859. ISSN 0004-5411. S2CID 14058631.
  3. [3]
    Nieuwenhuis, Robert; Oliveras, Albert (2005). Etessami, Kousha; Rajamani, Sriram K. (eds.). DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. Lecture Notes in Computer Science. Vol. 3576. Springer Berlin Heidelberg. pp. 321–334. doi:10.1007/11513988_33. ISBN 9783540316862. {{cite book}}: |journal= ignored (help)
  4. [4]
    Reynolds, Andrew (2015). "Satisfiability Modulo Theories and DPLL(T)" (PDF). The University of Iowa. Retrieved 2019-04-08.
  5. [5]
    de Moura, Leonardo; Bjørner, Nikolaj (2008). Ramakrishnan, C. R.; Rehof, Jakob (eds.). Z3: An Efficient SMT Solver. Lecture Notes in Computer Science. Vol. 4963. Springer Berlin Heidelberg. pp. 337–340. doi:10.1007/978-3-540-78800-3_24. ISBN 9783540788003. {{cite book}}: |journal= ignored (help)
  6. [6]
    Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014). Biere, Armin; Bloem, Roderick (eds.). A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 646–662. doi:10.1007/978-3-319-08867-9_43. ISBN 978-3-319-08867-9. {{cite book}}: |journal= ignored (help)
  7. [7]
    Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto (2008). Gupta, Aarti; Malik, Sharad (eds.). The MathSAT 4 SMT Solver. Lecture Notes in Computer Science. Vol. 5123. Springer Berlin Heidelberg. pp. 299–303. doi:10.1007/978-3-540-70545-1_28. ISBN 9783540705451. {{cite book}}: |journal= ignored (help)
P ≟ NP 

This theoretical computer science–related article is a stub. You can help Wikipedia by expanding it.
Share this article:

This article uses material from the Wikipedia article DPLL(T), and is written by contributors. Text is available under a CC BY-SA 4.0 International License; additional terms may apply. Images, videos and audio are available under their respective licenses.