DPLL(T)
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)