Algoritmy pro reprezentaci znalostí - NTIN099

• Anglický název: Algorithms for knowledge representation
• Zajišťuje: Katedra teoretické informatiky a matematické logiky (32-KTIML)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2020
• Semestr: letní
• E-Kredity: 3
• Rozsah, examinace: letní s.:2/0, Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: čeština, angličtina
• Způsob výuky: prezenční
• Další informace: http://ktiml.mff.cuni.cz/~kucerap/abf/
• Garant: RNDr. Petr Kučera, Ph.D.
• Vyučující: RNDr. Petr Kučera, Ph.D.
• Třída: Informatika Mgr. - volitelný; Informatika Mgr. - Teoretická informatika
• Kategorizace předmětu: Informatika > Informatika, Aplikační software, Počítačová grafika a geometrie, Databázové systémy, Didaktika informatiky, Diskrétní matematika, Předměty širšího základu, Předměty obecného základu, Počítačová a formální lingvistika, Optimalizace, Programování, Softwarové inženýrství, Teoretická informatika

Anotace

čeština

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.

Poslední úprava: Töpfer Pavel, doc. RNDr., CSc. (01.02.2019)

angličtina

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.

Poslední úprava: Töpfer Pavel, doc. RNDr., CSc. (01.02.2019)

Cíl předmětu

čeština

TBA

Poslední úprava: Hric Jan, RNDr. (07.06.2019)

Podmínky zakončení předmětu

čeština

TBA

Poslední úprava: Hric Jan, RNDr. (07.06.2019)

Literatura

čeština

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

Poslední úprava: T_KTI (27.02.2014)

Sylabus

čeština

• 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ů

Poslední úprava: Töpfer Pavel, doc. RNDr., CSc. (01.02.2019)

angličtina

• 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

Poslední úprava: Töpfer Pavel, doc. RNDr., CSc. (01.02.2019)