Wikipedista:Jj14/DPLL(T): Porovnání verzí

Smazaný obsah Přidaný obsah

V textu

Verze z 23. 2. 2024, 02:51

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 Microsoft 's Z3 Theorem Prover a CVC4, používá DPLL(T) jako základní techniku při řešení. ^[1] ^[2] ^[3]

Reference

↑ [s.l.]: [s.n.] ISBN 9783540788003. DOI 10.1007/978-3-540-78800-3_24. (anglicky)
↑ [s.l.]: [s.n.] ISBN 978-3-319-08867-9. DOI 10.1007/978-3-319-08867-9_43. (anglicky)
↑ [s.l.]: [s.n.] ISBN 9783540705451. DOI 10.1007/978-3-540-70545-1_28. (anglicky)

[1] [s.l.]: [s.n.] ISBN 9783540788003. DOI 10.1007/978-3-540-78800-3_24. (anglicky)

[2] [s.l.]: [s.n.] ISBN 978-3-319-08867-9. DOI 10.1007/978-3-319-08867-9_43. (anglicky)

[3] [s.l.]: [s.n.] ISBN 9783540705451. DOI 10.1007/978-3-540-70545-1_28. (anglicky)

[1]

[2]

[3]