..:: Martin Kot ::..
Automatizované řešení úloh s omezeními - šk. rok 2015/16
Obecné údaje
Garant: 
Počet kreditů:  4
Rozsah:  2/2/0/0
Ukončení:  Klasifikovaný zápočet
Oficiální stránka:  http://www.cs.vsb.cz/kot/ARUO/
Přednášející: 
Cvičící: 
 
Rozdělení bodů
Klasifikovaný zápočet: 
  • 60b - domácí úkol
  • 40b - zápočtová písemka
  • Podmínkou na zápočet je získání alespoň 31 bodů z domácího úkolu a alespoň 20 bodů ze zápočtové písemky
 
Anotace
Mnoho praktických problémů má jeden společný rys - vhodné řešení musí splňovat řadu z reality plynoucích omezení (rozvrh výuky, plán pracovní činnosti, přidělení rádiových frekvencí, ...). V posledních několika desetiletích se rozvinula oblast nazvaná "constraint processing", která rozvíjí obecné formy popisu takových omezení a zkoumá obecné metody řešení. Instance těchto metod se úspěšně používají v řadě odlišných oborů, od molekulární biologie, přes počítačovou grafiku, zpracování přirozeného jazyka až po např. návrh logických obvodů. Cílem tohoto předmětu je představit studentům na zvolených praktických problémech možné způsoby popisu omezení a vybrané metody hledání řešení vyhovujících těmto omezením. Současně praktické řešení takových problémů vyzkoušejí na cvičeních a v rámci semestrálního projektu, s pomocí volně dostupných knihoven a softwarových nástrojů (jako jsou například "SAT-solvers", tedy řešiče splnitelnosti booleovských omezení).
 
Rozvrh hodin
7:15
8:00
8:00
8:45
9:00
9:45
9:45
10:30
10:45
11:30
11:30
12:15
12:30
13:15
13:15
14:00
14:15
15:00
15:00
15:45
16:00
16:45
16:45
17:30
17:45
18:30
18:30
19:15
pondělí                            
úterý                            
středa                            
čtvrtek        
EB207
Kot M.
EB207
Kot M.
           
pátek                            
sobota                            
 
Přednášky
  • Praktické příklady problémů s omezeními a nástin obecných metod řešení. Exaktní formulace problémů, ilustrovaná na příkladu přidělování rádiových frekvencí; volba proměnných a jejich omezení.
  • Struktura prostoru potenciálních řešení. Metody šíření omezení (constraint propagation).
  • Obecné metody prohledávání prostoru potenciálních řešení.
  • Problém rozvrhování (výuky, prac. směn,...). Ilustrace použití vybraných metod.
  • Formulace problému ověření funkce logického obvodu a dalších problémů převeditelných na problém SAT (splnitelnost booleovských formulí). Řešiče SAT (SAT-solvers).
  • Metody používané v řešičích SAT.
  • Stochastické metody prohledávání.
  • Kombinatorická optimalizace. Multikomoditní toky, logistické problémy.
  • Celočíselná lineární omezení a specifické metody řešení.
  • Plánování (přidělování úloh procesorům).
  • Nástin vybraných pokročilých partií (metody dekompozice, pravděpodobnostní sítě,...).
  • Metody kombinující prohledávání a šíření omezení.
  • Shrnutí, zopakování.
 
Studijní literatura
  • R. Dechter: Constraint processing, Morgan Kaufmann, 2003
Literatura není povinná, na přednáškách a cvičeních se dozvíte vše potřebné. (Toto není recitační kroužek, takže se nemusíte učit nazpaměť pasáže z knih. Lépe řečeno, nazpaměť se ani učit nesmíte, látce je třeba porozumět.)