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
theoryT.[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]
^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.
ISBN9783540278139. {{
cite book}}: |journal= ignored (
help)
^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.
ISSN0004-5411.
S2CID14058631.
^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.
ISBN9783540316862. {{
cite book}}: |journal= ignored (
help)
^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.
ISBN9783540788003. {{
cite book}}: |journal= ignored (
help)
^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.
ISBN978-3-319-08867-9. {{
cite book}}: |journal= ignored (
help)