Wikipedista:Jj14/DPLL(T)
V informatice je DPLL(T) technika pro stanovení splnitelnosti problémů SMT (splnitelnost modulo teorie). Algoritmus rozšiřuje původní DPLL algoritmus pro řešení SAT o schopnost odvozovat v libovolné teorii T.[1][2][3] Na vysoké úrovni algoritmus funguje tak, že transformuje SMT problém na SAT formuli, kde jsou atomické formule teorie T nahrazeny booleovskými proměnnými. Algoritmus opakovaně najde splňující ohodnocení SAT problému, následně požádá řešič teorie, aby zkontroloval konzistenci v rámci doménově specifické teorie, a poté (pokud je nalezen spor) zpřesní SAT formuli o tyto informace.[4]
Mnoho moderních SMT řešičů, jako je Z3 Theorem Prover od Microsoftu a CVC4, používá DPLL(T) jako základní techniku při řešení.[5][6][7]
Reference[editovat | editovat zdroj]
- ↑ GANZINGER, Harald; HAGEN, George; NIEUWENHUIS, Robert; OLIVERAS, Albert; TINELLI, Cesare. DPLL(T): Fast Decision Procedures. Redakce Alur Rajeev. [s.l.]: Springer Berlin Heidelberg, 2004. (Lecture Notes in Computer Science; sv. 3114). ISBN 9783540278139. DOI 10.1007/978-3-540-27813-9_14. S. 175–188. (anglicky)
- ↑ NIEUWENHUIS, Robert; OLIVERAS, Albert; TINELLI, Cesare. Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T). J. ACM. 2006, s. 937–977. ISSN 0004-5411. DOI 10.1145/1217856.1217859. S2CID 14058631.
- ↑ NIEUWENHUIS, Robert; OLIVERAS, Albert. DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. Redakce Etessami Kousha. [s.l.]: Springer Berlin Heidelberg, 2005. (Lecture Notes in Computer Science; sv. 3576). ISBN 9783540316862. DOI 10.1007/11513988_33. S. 321–334. (anglicky)
- ↑ REYNOLDS, Andrew. Satisfiability Modulo Theories and DPLL(T) [online]. 2015 [cit. 2019-04-08]. Dostupné online.
- ↑ DE MOURA, Leonardo; BJØRNER, Nikolaj. Z3: An Efficient SMT Solver. Redakce Ramakrishnan C. R.. [s.l.]: Springer Berlin Heidelberg, 2008. (Lecture Notes in Computer Science; sv. 4963). ISBN 9783540788003. DOI 10.1007/978-3-540-78800-3_24. S. 337–340. (anglicky)
- ↑ LIANG, Tianyi; REYNOLDS, Andrew; TINELLI, Cesare; BARRETT, Clark; DETERS, Morgan. A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. Redakce Biere Armin. Cham: Springer International Publishing, 2014. (Lecture Notes in Computer Science). ISBN 978-3-319-08867-9. DOI 10.1007/978-3-319-08867-9_43. S. 646–662. (anglicky)
- ↑ BRUTTOMESSO, Roberto; CIMATTI, Alessandro; FRANZÉN, Anders; GRIGGIO, Alberto; SEBASTIANI, Roberto. The MathSAT 4 SMT Solver. Redakce Gupta Aarti. [s.l.]: Springer Berlin Heidelberg, 2008. (Lecture Notes in Computer Science; sv. 5123). ISBN 9783540705451. DOI 10.1007/978-3-540-70545-1_28. S. 299–303. (anglicky)
V tomto článku byl použit překlad textu z článku DPLL(T) na anglické Wikipedii (číslo revize nebylo určeno).