SAT solvery

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ć.