DPLL (T) - DPLL(T) - Wikipedia

V počítačové vědě DPLL (T) je rámec pro určování splnitelnosti SMT problémy. Algoritmus rozšiřuje originál SAT -Řešení Algoritmus DPLL se schopností svévolně uvažovat teorie T.[1][2][3] Na vysoké úrovni algoritmus funguje tak, že transformuje problém SMT na vzorec SAT, kde jsou atomy nahrazeny booleovskými proměnnými. Algoritmus opakovaně najde uspokojivé ocenění problému SAT, konzultuje a řešitel teorie zkontrolovat konzistenci podle teorie specifické pro doménu a poté (je-li nalezen rozpor) vylepšit vzorec SAT s touto informací.[4]

Mnoho moderních řešitelů SMT, jako např Microsoft je Poskytovatel věty Z3, používají DPLL (T) k napájení svých schopností řešení jádra.[5][6]

Reference

  1. ^ Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2004). Alur, Rajeev; Peled, Doron A. (eds.). „DPLL (T): Fast Decision Procedures“. Ověření pomocí počítače. Přednášky z informatiky. Springer Berlin Heidelberg. 3114: 175–188. doi:10.1007/978-3-540-27813-9_14. ISBN  9783540278139.
  2. ^ Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2006). „Řešení teorií SAT a SAT: od abstraktního postupu Davis – Putnam – Logemann – Loveland po 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) s vyčerpávajícím rozšířením teorie a její aplikace na logiku rozdílu“. Ověření pomocí počítače. Přednášky z informatiky. Springer Berlin Heidelberg. 3576: 321–334. doi:10.1007/11513988_33. ISBN  9783540316862.
  4. ^ Reynolds, Andrew (2015). „Teorie uspokojivosti modulo a DPLL (T)“ (PDF). University of Iowa. Citováno 2019-04-08.
  5. ^ de Moura, Leonardo; Bjørner, Nikolaj (2008). Ramakrishnan, C. R .; Rehof, Jakob (eds.). „Z3: Efektivní řešení SMT“. Nástroje a algoritmy pro konstrukci a analýzu systémů. Přednášky z informatiky. Springer Berlin Heidelberg. 4963: 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.). „Řešitel MathSAT 4 SMT“. Ověření pomocí počítače. Přednášky z informatiky. Springer Berlin Heidelberg. 5123: 299–303. doi:10.1007/978-3-540-70545-1_28. ISBN  9783540705451.