DPLL(T)
 | This article, DPLL(T), has recently been created via the Articles for creation process. Please check to see if the reviewer has accidentally left this template after accepting the draft and take appropriate action as necessary.
Reviewer tools: Inform author |
DPLL(T) is a framework for determining the satsfiability of SMT problems. The algorithm extends the original DPLL SAT-solving 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 simplified SAT formula. The algorithm repeatedly finds a satifsying valuation for the SAT problem, consults a theory solver to find domain-specific logical contradictions and then refines the SAT formula with this information. [4]
Many modern SMT solvers, such as Microsoft's Z3, use DPLL(T) to power their core solving capabilities. [5][6]
See also
References
- ^ Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2004). Alur, Rajeev; Peled, Doron A. (eds.). "DPLL(T): Fast Decision Procedures". Computer Aided Verification. Lecture Notes in Computer Science. Springer Berlin Heidelberg: 175–188. doi:10.1007/978-3-540-27813-9_14. ISBN 9783540278139.
- ^ 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.
- ^ Nieuwenhuis, Robert; Oliveras, Albert (2005). Etessami, Kousha; Rajamani, Sriram K. (eds.). "DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic". Computer Aided Verification. Lecture Notes in Computer Science. Springer Berlin Heidelberg: 321–334. doi:10.1007/11513988_33. ISBN 9783540316862.
- ^ Reynolds, Andrew (2015). "Satisfiability Modulo Theories and DPLL(T)" (PDF). The University of Iowa. Retrieved 2019-04-08.
{{cite web}}: Cite has empty unknown parameter:|dead-url=(help) - ^ de Moura, Leonardo; Bjørner, Nikolaj (2008). Ramakrishnan, C. R.; Rehof, Jakob (eds.). "Z3: An Efficient SMT Solver". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Springer Berlin Heidelberg: 337–340. doi:10.1007/978-3-540-78800-3_24. ISBN 9783540788003.
- ^ Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto (2008). Gupta, Aarti; Malik, Sharad (eds.). "The MathSAT 4 SMT Solver". Computer Aided Verification. Lecture Notes in Computer Science. Springer Berlin Heidelberg: 299–303. doi:10.1007/978-3-540-70545-1_28. ISBN 9783540705451.
{{cite journal}}: no-break space character in|title=at position 12 (help)