SAT solvery

Prelegent(ci)

Tadeusz Sznuk

Afiliacja

Uniwersytet Warszawski

Termin

21 marca 2011 10:15

Pokój

p. 4790

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

SAT-solver, jaki jest, każdy widzi. Ale nie każdy przygląda się uważnie. Dlatego zamierzam opowiedzieć, co to dokładnie jest SAT-solver i jakie problemy można za pomocą takowego rozwiązywać  Postaram się omówić dość szczegółowo architekturę CDCL, czyli najpopularniejszy ostatnio rodzaj solverów, a także wspomnieć o kilku innych podejściach, i jakoś to wszystko porównać. Głównym celem prezentacji jest wywołanie dyskusji o tym, co ciekawego (tz. nowego) możnaby w tym temacie zrobić.

---