Syllabus
- Exponential algorithms for k-SAT and SAT
- Paremetrized algorithms for SAT based on backdoor sets
- Algorithms for SAT parameterized with treewidth
- Kernelization for MaxSAT and parameterization of MaxSAT
- Algorithms for MaxSAT based on branch and bound
- Algorithms for #SAT (model counting)
- Knowledge representation based on NNF (negation normal form)
- OBDD, DNNF, d-DNNF, SDD
- Comparing various versions of NNF with respect to query answering and succintness
- Compilation of a CNF formula into DNNFs and its variants.
- Application to model counting
Annotation
The purpose of the lecture is to teach several algorithms for various problems related to boolean functions, especially SAT (satisfiability).
Algorithms for SAT with exponential worst-case running time. Parameterized algorithms for SAT and MaxSAT. Search algorithms for MaxSAT. Knowledge representation based on NNF.