DPLL(T)

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. 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.

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

References

  1. ↑ Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2004). "DPLL(T): Fast Decision Procedures". In Alur, Rajeev; Peled, Doron A. (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 3114. Springer Berlin Heidelberg. pp. 175–188. doi:10.1007/978-3-540-27813-9_14. ISBN 9783540278139.
  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. ↑ Nieuwenhuis, Robert; Oliveras, Albert (2005). "DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic". In Etessami, Kousha; Rajamani, Sriram K. (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 3576. Springer Berlin Heidelberg. pp. 321–334. doi:10.1007/11513988_33. ISBN 9783540316862.
  4. ↑ Reynolds, Andrew (2015). "Satisfiability Modulo Theories and DPLL(T)" (PDF). The University of Iowa. Retrieved 2019-04-08.
  5. ↑ de Moura, Leonardo; Bjørner, Nikolaj (2008). "Z3: An Efficient SMT Solver". In Ramakrishnan, C. R.; Rehof, Jakob (eds.). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 4963. Springer Berlin Heidelberg. pp. 337–340. doi:10.1007/978-3-540-78800-3_24. ISBN 9783540788003.
  6. ↑ Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014). "A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions". In Biere, Armin; Bloem, Roderick (eds.). Computer Aided Verification. 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.
  7. ↑ Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto (2008). "The MathSAT 4 SMT Solver". In Gupta, Aarti; Malik, Sharad (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 5123. Springer Berlin Heidelberg. pp. 299–303. doi:10.1007/978-3-540-70545-1_28. ISBN 9783540705451.