Sylabus
- Exponenciální algoritmy pro k-SAT a obecný SAT
- Parametrizované algoritmy pro SAT založené na backdoor množinách.
- Algoritmy pro SAT parametrizované stromovou šířkou
- Kernelizace pro MaxSAT a parametrizace MaxSAT
- Algoritmy pro MaxSAT založené na větvení a prořezávání (branch & bound)
- Algoritmy pro #SAT
- Reprezentace znalostí založené na NNF (negation normal form)
- OBDD, DNNF, d-DNNF, SDD
- Srovnání těchto reprezentací s ohledem na zodpovídání dotazů a velikost
- Kompilace formule v KNF do různých typů reprezentací
- Využití pro počítání modelů
Anotace
Přednáška seznamující s některými algoritmy pro booleovské funkce, zejména splnitelnost. Exponenciální algoritmy pro splnitelnost. Parametrizované algoritmy pro splnitelnost a MaxSAT. Prohledávací algoritmy pro
MaxSAT. Reprezentace znalostí založené na NNF.