Přeskočit na obsah

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

Z Wikipedie, otevřené encyklopedie
Smazaný obsah Přidaný obsah
vytvořeno překladem stránky „DPLL(T)
značky: nezformátované reference editace z rozšíření Překlad Překlad 2
(Žádný rozdíl)

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

  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)