460-4089/01 – Automatizované řešení úloh s omezeními (ARUO)
Garantující katedra | Katedra informatiky | Kredity | 4 |
Garant předmětu | Ing. Martin Kot, Ph.D. | Garant verze předmětu | Ing. Martin Kot, Ph.D. |
Úroveň studia | pregraduální nebo graduální | Povinnost | povinně volitelný |
Ročník | 1 | Semestr | zimní |
| | Jazyk výuky | čeština |
Rok zavedení | 2015/2016 | Rok zrušení | 2022/2023 |
Určeno pro fakulty | FEI | Určeno pro typy studia | navazující magisterské, magisterské |
Cíle předmětu vyjádřené dosaženými dovednostmi a kompetencemi
Student po úspěšném absolvování předmětu:
- rozumí základním pojmům z oblasti "constraint processing"
- umí klasifikovat praktické problémy spadající do dané oblasti
- umí k praktickému problému nalézt relevantní proměnné a exaktně zformulovat příslušná omezení
- má přehled o obecných metodách řešení
- má přehled o dostupných softwarových nástrojích pro řešení úloh s omezeními
- má zkušenost s vyřešením praktického problému s pomocí jednoho z těchto nástrojů
Vyučovací metody
Přednášky
Cvičení (v učebně)
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ě si praktické řešení takových problémů vyzkoušejí na cvičeních a v rámci domácího úkolu, 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í).
Povinná literatura:
- Rina Dechter: Constraint Processing, Morgan Kaufmann, 2003
Doporučená literatura:
- Krzysztof Apt: Principles of Constraint Programming, Cambridge University
Press, 2003.
- Malik Ghallab, Dana Nau, Paolo Traverso: Automated Planning: Theory & Practice,
Morgan Kaufmann, 2004.
- Christos H. Papadimitriou, Kenneth Steiglitz: Combinatorial Optimization:
Algorithms and Complexity, Dover Publications, 1998.
- Alexander Schrijver: Combinatorial Optimization (3 volume, A,B, & C),
Springer, 2003.
- Daniel Kroening, Ofer Strichman: Decision Procedures: An Algorithmic Point of View,
Springer, 2008.
Forma způsobu ověření studijních výsledků a další požadavky na studenta
Řešení a diskuse zadaných úloh pro jednotlivá cvičení.
Zpracování domácího úkolu, zakončeného individuální písemnou zprávou.
Závěrečná zápočtová písemka.
E-learning
Electronic materials underlying the lectures and tutorials, pointers to software tools, and futher information are accessible from the course web-page.
Další požadavky na studenta
Další požadavky na studenta nejsou kladeny.
Prerekvizity
Předmět nemá žádné prerekvizity.
Korekvizity
Předmět nemá žádné korekvizity.
Osnova předmětu
Osnova přednášek:
1. Praktické příklady problémů s omezeními a nástin obecných metod řešení. Exaktní formulace problémů ilustrovaná na příkladu Huffmanovo-Clowesova ohodnocení scény.
2. Sítě omezení a jejich grafové reprezentace, speciální tvary sítí.
3. Šíření omezení (hranová konzistentnost, globální omezení), příslušné algoritmy.
4. Řešení úloh pomocí backtrackingu, algoritmy pro zlepšení dopředné fáze backtrackingu.
5. Algoritmy pro zlepšení zpětné fáze backtrackingu.
6. Problém SAT, jeho NP-úplnost, využití SATu při řešení úloh s omezeními.
7. Polynomiálně řešitelné varianty problému SAT, příslušné polynomiální algoritmy.
8. Řešení obecného problému SAT, algoritmy DPLL, stochastické, ...
9. Optimalizační problémy, využití backtrackingu (Branch and Bound), metody eliminace košíků.
10. Využití pravděpodobnostních sítí pro nejistá omezení (na příkladu medicinských diagnóz).
11. Plánování, rozvrhování - možná paradigmata, varianty kriteriální funkce.
12. Aproximační algoritmy (na příkladu problému obchodního cestujícího).
13. Shrnutí učiva, stručný přehled dalších možných témat z oblasti úloh s omezeními.
Osnova cvičení na počítačové učebně:
1. Procvičení exaktní formulace problémů. Úvodní seznámení s nástrojem Gecode - řešičem úloh s omezeními.
2. Gecode - tvorba modelu problému.
3. Gecode - využití různých metod prohledávání implementovaných v tomto nástroji.
4. Formulace problému ve formě vstupu po řešič SAT. Úvodní seznámení s MiniSAT - jednoduchým řešičem SAT.
5. Řešení praktických problémů za pomocí MiniSAT.
6. Stochastické metody prohledávání. Práce se stochastickými řešiči SAT.
7. Nástroje pro řešení SAT při tvorbě vlastních programů.
8. Další dostupné řešiče SAT, jejich společné a odlišné rysy, přehled formátů vstupních souborů pro řešiče SAT.
9.-10. Jiné dostupné softwarové nástroje pro řešení úloh s omezeními, jejich přehled, možnosti, vlastnosti.
11. Konzultace domácích úkolů.
12. Odevzdání domácích úkolů.
13. Písemný zápočtový test.
Podmínky absolvování předmětu
Výskyt ve studijních plánech
Výskyt ve speciálních blocích
Hodnocení Výuky
Předmět neobsahuje žádné hodnocení.