Algorithms for knowledge representation - NTIN099
Title: Algoritmy pro reprezentaci znalostí
Guaranteed by: Department of Theoretical Computer Science and Mathematical Logic (32-KTIML)
Faculty: Faculty of Mathematics and Physics
Actual: from 2020
Semester: summer
E-Credits: 3
Hours per week, examination: summer s.:2/0, Ex [HT]
Capacity: unlimited
Min. number of students: unlimited
4EU+: no
Virtual mobility / capacity: no
State of the course: taught
Language: Czech, English
Teaching methods: full-time
Teaching methods: full-time
Additional information: http://ktiml.mff.cuni.cz/~kucerap/abf/
Guarantor: RNDr. Petr Kučera, Ph.D.
Class: Informatika Mgr. - volitelný
Informatika Mgr. - Teoretická informatika
Classification: Informatics > Informatics, Software Applications, Computer Graphics and Geometry, Database Systems, Didactics of Informatics, Discrete Mathematics, External Subjects, General Subjects, Computer and Formal Linguistics, Optimalization, Programming, Software Engineering, Theoretical Computer Science
Opinion survey results   Examination dates   SS schedule   Noticeboard   
Annotation -
Last update: doc. RNDr. Pavel Töpfer, CSc. (01.02.2019)
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.
Aim of the course -
Last update: RNDr. Jan Hric (07.06.2019)

TBA

Course completion requirements -
Last update: RNDr. Jan Hric (07.06.2019)

TBA

Literature -
Last update: T_KTI (27.02.2014)

A. Biere, M. Heule, H. van Maaren, T. Walsh (Eds.). Handbook of Satisfiability, in: Frontiers in Artificial Intelligence and Applications, vol. 185, IOS Press, 2009, pp. 131-153

Niedermeier, Rolf. Invitation to fixed-parameter algorithms. Vol. 3. Oxford: Oxford University Press, 2006

Flum, Jörg, and Martin Grohe. Parameterized complexity theory. Vol. 3. Heidelberg: Springer, 2006

Syllabus -
Last update: doc. RNDr. Pavel Töpfer, CSc. (01.02.2019)
  • 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