SubjectsSubjects(version: 901)
Course, academic year 2022/2023
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 [hours/week]
Capacity: unlimited
Min. number of students: unlimited
Virtual mobility / capacity: no
State of the course: taught
Language: Czech, English
Teaching methods: full-time
Additional information:
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
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)


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


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)
  • Comparing various versions of NNF with respect to query answering and


  • Compilation of a CNF formula into DNNFs and its variants.
  • Application to model counting

Charles University | Information system of Charles University |