Jump to content

DPLL(T): Difference between revisions

Add links
From Wikipedia, the free encyclopedia
Browse history interactively
← Previous editNext edit →
Content deleted Content added
VisualWikitext
m Adam Williams moved page Draft:DPLL(T) to DPLL(T): Backlog too big for AfC process, no desire to wait 3 months
m Remove AfC tag
Line 1: Line 1:
{{AFC submission|||ts=20190408150930|u=Adam Williams|ns=118}}

DPLL(T) is a framework for determining the satsfiability of [[Satisfiability modulo theories|SMT]] problems. The algorithm extends the original [[DPLL algorithm|DPLL]] [[Boolean satisfiability problem|SAT]]-solving algorithm with the ability to reason about an arbitrary theory ''T''. <ref>{{Cite journal|last=Ganzinger|first=Harald|last2=Hagen|first2=George|last3=Nieuwenhuis|first3=Robert|last4=Oliveras|first4=Albert|last5=Tinelli|first5=Cesare|date=2004|editor-last=Alur|editor-first=Rajeev|editor2-last=Peled|editor2-first=Doron A.|title=DPLL(T): Fast Decision Procedures|url=https://link.springer.com/chapter/10.1007/978-3-540-27813-9_14|journal=Computer Aided Verification|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=175–188|doi=10.1007/978-3-540-27813-9_14|isbn=9783540278139}}</ref><ref>{{Cite journal|last=Nieuwenhuis|first=Robert|last2=Oliveras|first2=Albert|last3=Tinelli|first3=Cesare|date=2006|title=Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T)|url=http://doi.acm.org/10.1145/1217856.1217859|journal=J. ACM|volume=53|issue=6|pages=937–977|doi=10.1145/1217856.1217859|issn=0004-5411}}</ref><ref>{{Cite journal|last=Nieuwenhuis|first=Robert|last2=Oliveras|first2=Albert|date=2005|editor-last=Etessami|editor-first=Kousha|editor2-last=Rajamani|editor2-first=Sriram K.|title=DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic|url=https://link.springer.com/chapter/10.1007/11513988_33|journal=Computer Aided Verification|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=321–334|doi=10.1007/11513988_33|isbn=9783540316862}}</ref> 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. <ref>{{Cite web|url=http://homepage.divms.uiowa.edu/~ajreynol/pres-dpllt15.pdf|title=Satisfiability Modulo Theories and DPLL(T)|last=Reynolds|first=Andrew|date=2015|website=The University of Iowa|archive-url=|archive-date=|dead-url=|access-date=2019-04-08}}</ref>
DPLL(T) is a framework for determining the satsfiability of [[Satisfiability modulo theories|SMT]] problems. The algorithm extends the original [[DPLL algorithm|DPLL]] [[Boolean satisfiability problem|SAT]]-solving algorithm with the ability to reason about an arbitrary theory ''T''. <ref>{{Cite journal|last=Ganzinger|first=Harald|last2=Hagen|first2=George|last3=Nieuwenhuis|first3=Robert|last4=Oliveras|first4=Albert|last5=Tinelli|first5=Cesare|date=2004|editor-last=Alur|editor-first=Rajeev|editor2-last=Peled|editor2-first=Doron A.|title=DPLL(T): Fast Decision Procedures|url=https://link.springer.com/chapter/10.1007/978-3-540-27813-9_14|journal=Computer Aided Verification|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=175–188|doi=10.1007/978-3-540-27813-9_14|isbn=9783540278139}}</ref><ref>{{Cite journal|last=Nieuwenhuis|first=Robert|last2=Oliveras|first2=Albert|last3=Tinelli|first3=Cesare|date=2006|title=Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T)|url=http://doi.acm.org/10.1145/1217856.1217859|journal=J. ACM|volume=53|issue=6|pages=937–977|doi=10.1145/1217856.1217859|issn=0004-5411}}</ref><ref>{{Cite journal|last=Nieuwenhuis|first=Robert|last2=Oliveras|first2=Albert|date=2005|editor-last=Etessami|editor-first=Kousha|editor2-last=Rajamani|editor2-first=Sriram K.|title=DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic|url=https://link.springer.com/chapter/10.1007/11513988_33|journal=Computer Aided Verification|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=321–334|doi=10.1007/11513988_33|isbn=9783540316862}}</ref> 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. <ref>{{Cite web|url=http://homepage.divms.uiowa.edu/~ajreynol/pres-dpllt15.pdf|title=Satisfiability Modulo Theories and DPLL(T)|last=Reynolds|first=Andrew|date=2015|website=The University of Iowa|archive-url=|archive-date=|dead-url=|access-date=2019-04-08}}</ref>


Revision as of 15:11, 8 April 2019

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

  1. ^ 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.
  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.
  3. ^ 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.
  4. ^ 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)
  5. ^ 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.
  6. ^ 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)
P ≟ NP 

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

Retrieved from "https://en.wikipedia.org/enwiki/w/index.php?title=DPLL(T)&oldid=891531232"