Wikipedista:Jj14/DPLL(T): Porovnání verzí
Smazaný obsah Přidaný obsah
vytvořeno překladem stránky „DPLL(T)“ |
posteditace překladu |
||
| Řádek 1: | Řádek 1: | ||
{{Upravit|poznámky=prosim, kat., ref.}} |
{{Upravit|poznámky=prosim, kat., ref.}} |
||
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. |
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é [[teorie|teorii]] T.<ref>{{Cite book|last1=Ganzinger|first1=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|journal=Computer Aided Verification|volume=3114|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|doi-access=free}}</ref><ref>{{Cite journal|last1=Nieuwenhuis|first1=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)|journal=J. ACM|volume=53|issue=6|pages=937–977|doi=10.1145/1217856.1217859|s2cid=14058631 |issn=0004-5411}}</ref><ref>{{Cite book|last1=Nieuwenhuis|first1=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|journal=Computer Aided Verification|volume=3576|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=321–334|doi=10.1007/11513988_33|isbn=9783540316862|doi-access=free}}</ref> 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.<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=|access-date=2019-04-08}}</ref> |
||
Mnoho moderních SMT řešičů, jako je [[Z3 Theorem Prover]] od [[Microsoft]]u a [[CVC4]], používá DPLL(T) jako základní techniku při řešení.<ref>{{Cite book|last1=de Moura|first1=Leonardo|last2=Bjørner|first2=Nikolaj|date=2008|editor-last=Ramakrishnan|editor-first=C. R.|editor2-last=Rehof|editor2-first=Jakob|title=Z3: An Efficient SMT Solver|journal=Tools and Algorithms for the Construction and Analysis of Systems|volume=4963|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=337–340|doi=10.1007/978-3-540-78800-3_24|isbn=9783540788003|doi-access=free}}</ref><ref>{{Cite book |last1=Liang |first1=Tianyi |last2=Reynolds |first2=Andrew |last3=Tinelli |first3=Cesare |last4=Barrett |first4=Clark |last5=Deters |first5=Morgan |date=2014 |editor-last=Biere |editor-first=Armin |editor2-last=Bloem |editor2-first=Roderick |title=A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions |journal=Computer Aided Verification |series=Lecture Notes in Computer Science |language=en |location=Cham |publisher=Springer International Publishing |pages=646–662 |doi=10.1007/978-3-319-08867-9_43 |isbn=978-3-319-08867-9|doi-access=free }}</ref><ref>{{Cite book|last1=Bruttomesso|first1=Roberto|last2=Cimatti|first2=Alessandro|last3=Franzén|first3=Anders|last4=Griggio|first4=Alberto|last5=Sebastiani|first5=Roberto|date=2008|editor-last=Gupta|editor-first=Aarti|editor1-link=Aarti Gupta (computer scientist)|editor2-last=Malik|editor2-first=Sharad|title=The MathSAT 4 SMT Solver|journal=Computer Aided Verification|volume=5123|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=299–303|doi=10.1007/978-3-540-70545-1_28|isbn=9783540705451|doi-access=free}}</ref> |
|||
Mnoho moderních SMT řešičů, jako je [[Microsoft]] 's Z3 Theorem Prover a CVC4, používá DPLL(T) jako základní techniku při řešení. <ref>{{Citace monografie |
|||
| isbn = 9783540788003 |
|||
| doi = 10.1007/978-3-540-78800-3_24 |
|||
| jazyk = en |
|||
| url-access = free |
|||
}}</ref> <ref>{{Citace monografie |
|||
| isbn = 978-3-319-08867-9 |
|||
| doi = 10.1007/978-3-319-08867-9_43 |
|||
| jazyk = en |
|||
| url-access = free |
|||
}}</ref> <ref>{{Citace monografie |
|||
| isbn = 9783540705451 |
|||
| doi = 10.1007/978-3-540-70545-1_28 |
|||
| jazyk = en |
|||
| url-access = free |
|||
}}</ref> |
|||
== Reference == |
== Reference == |
||
<references /> |
|||
{{překlad|en|DPLL(T)}} |
|||
Verze z 23. 2. 2024, 03:07
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
- ↑ 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).