|
Vyučující
|
|
|
|
Obsah předmětu
|
Obsahem předmětu jsou významné algoritmické problémy a k nim existující algoritmy. Cílem je seznámit studenty s procesem, kterým informatická komunita přichází na nové algoritmy pro důležité problémy tak, aby je poté mohli tuto zkušenost aplikovat na jiné problémy. Sylabus: - Problém splnitelnosti formulí výrokové logiky (SAT): odvození a implementace algoritmů od základních až k algoritmům používaných v průmyslových SAT solverech, použití SAT solverů pro praktické úlohy. - Problém grafového izomorfismu: colour refinement algoritmus, individualisation-refinement algoritmus. Nástroj nauty.
|
|
Studijní aktivity a metody výuky
|
|
Metody práce s textem (učebnicí, knihou), Demonstrace, Laborování
|
|
Výstupy z učení
|
Cílem je seznámit studenty s procesem, kterým informatická komunita přichází na nové algoritmy pro důležité problémy tak, aby je poté mohli tuto zkušenost aplikovat na jiné problémy.
|
|
Předpoklady
|
nespecifikováno
|
|
Hodnoticí metody a kritéria
|
Analýza výkonů studenta, Rozbor produktů pracovní činnosti studenta (technické práce)
Aktivní účast na hodině. Plnění úkolů.
|
|
Doporučená literatura
|
-
B.D. McKay A. Piperno. Practical graph isomorphism, II.
-
Biere A. et al (editors). (2009). Handbook of Satisfiability.
-
D. Knuth. (2015). The Art of Computer Programming, Volume 4, Fascicle 6. Satisfiability.
-
Matoušek, Nešetřil. (2002). Kapitoly z diskrétní matematiky.
|