|
Vyučující
|
|
|
|
Obsah předmětu
|
- Problém splnitelnosti formulí výrokové logiky (SAT), jeho obtížnost, aplikace a teoretický význam. - Rezoluce, věta o rezoluci, algoritmy odvozené od rezoluce, dolní omezení délky rezolučního zamítnutí. - Varianty řešitelné v polynomickém čase. - Rodina algoritmů založená na DPLL, hlavní myšlenky CDCL solverů. - Paturi-Pudlák-Zane algoritmus - Kombinatorické úvahy o splnitelnosti.
|
|
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 studenty seznámit s důležitým algoritmickým problémem, algoritmy pro jeho řešení, jejich implementačními aspekty a příslušnými teoretickými partiemi. Jako modelový problém je zvolena splnitelnost formulí výrokové logiky.
|
|
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.
|