460-4057/01 – Automatizované řešení úloh s omezeními (ARUO)
| Garantující katedra | Katedra informatiky | Kredity | 5 |
| Garant předmětu | prof. RNDr. Petr Jančar, CSc. | Garant verze předmětu | Ing. Martin Kot, Ph.D. |
| Úroveň studia | pregraduální nebo graduální | Povinnost | volitelný odborný |
| Ročník | 1 | Semestr | zimní |
| | Jazyk výuky | čeština |
| Rok zavedení | 2012/2013 | Rok zrušení | 2019/2020 |
| Určeno pro fakulty | FEI | Určeno pro typy studia | navazující 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ě)
Projekt
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í).
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
Zhodnocení vypracovaného projektu a zápočtová písemka.
E-learning
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 přidělování rádiových frekvencí; volba proměnných a jejich omezení.
2. Struktura prostoru potenciálních řešení.
Metody šíření omezení (constraint propagation).
3. Obecné metody prohledávání prostoru potenciálních řešení.
4. Problém rozvrhování (výuky, prac. směn,...).
Ilustrace použití vybraných metod.
5. 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).
6. Metody používané v řešičích SAT.
7. Stochastické metody prohledávání.
8. Kombinatorická optimalizace.
Multikomoditní toky, logistické problémy.
9. Celočíselná lineární omezení a specifické metody řešení.
10. Plánování (přidělování úloh procesorům).
11. Nástin vybraných pokročilých partií (metody dekompozice, pravděpodobnostní sítě,...).
12. Metody kombinující prohledávání a šíření omezení.
13. Shrnutí, zopakování
-----------------------------
Osnova počítačových cvičení:
----------------------------
Cvičení se zpravidla skládají ze dvou částí:
- u tabule (T) - 30-45 minut, rezebrání a procvičení metod z přednášek na dalších příkladech, případně dokončení řešení praktických příkladů z přednášek
- u počítače (P) - 45-60 minut, práce s dostupnými nástroji, v nichž jsou probírané metody implementovány, případně vlastní implementace jednodušších nástrojů za použití dostupných knihoven (např. Sat4j)
1. T: Exaktní formulace problémů
P: Úvodní seznámení s nástrojem Gecode - řešičem úloh s omezeními
2. T: Šíření omezení
P: Gecode - tvorba modelu problému
3. T: Prohledávání prostoru potenciálních řešení
P: Gecode - využití různých metod prohledávání implementovaných v tomto nástroji
4. T: Problém rozvrhování
P: Softwarové řešení problému rozvrhování
5. T: Formulace problému ve formě vstupu po řešič SAT
P: Úvodní seznámení s MiniSAT - jednoduchým řešičem SAT
6. T: Metody pro řešení SAT
P: Řešení praktických problémů za pomocí MiniSAT
7. T: Stochastické metody prohledávání
P: UBCSAT - stochastický řešič SAT
8. T: Logistické problémy, multikomoditní toky
P: Využití JAVA knihovny Sat4j pro řešení SAT při tvorbě vlastních programů
9. T: Řešení úloh celočíselného lineárního programování
P: Sat4j jako samostatný řešič SAT, další dostupné řešiče SAT, jejich společné a odlišné rysy
10. T: Problém plánování
P: Softwarové řešení úloh celočíselného lineárního programování
11. T: Dekompozice problémů, pravděpodobnostní sítě
P: Konzultace projektů
12. T: Využití metod kombinujících prohledávání a šíření omezení
P: Konzultace projektů
13. Zápočtová písemka
Osnova ostatní, projekty a indiv. práce studentů:
-------------------------------------------------
Každý student dostane slovně zadán nějaký problém a přidělen (volně dostupný) softwarový nástroj, s jehož pomocí jej má řešit (Gecode, Choco Solver, různé řešiče SAT, ...). Jeho úkolem bude:
1. Pokud půjde o nástroj neprobíraný podrobně na cvičeních (ale podobný těm probíraným), tak nastudovat tento nástroj (odlišnosti ve způsobu specifikace vstupního problému, formát výstupů apod. oproti nástrojům probíraným na cvičeních). V tomto případě bude zadaný problém jednodušší, aby se celková doba potřebná k vypracování projektu přibližně shodovala s řešením pomocí nástrojů používaným na cvičeních.
2. Formalizovat slovní zadání, tedy identifikovat proměnné, zapsat omezení vhodným formálním způsobem.
3. Vytvořit vstup pro přidělený nástroj (model pro Gecode, formuli ve správném formátu pro řešiče SAT,...), a s pomocí nástroje najít řešení.
4. Vyzkoušet různé heuristiky, metody propagace omezení apod. poskytované nástrojem a porovnat nalezené výsledky při takto odlišných nastaveních.
5. Interpretovat řešení - tedy převest nástrojem nalezené ohodnocení proměnných a podobné výstupy zpět do pojmů slovního zadání tak, aby tomu rozuměl člověk pohybující se v aplikační oblasti daného problému neznající teorii z oblasti constraint processing.
6. Vypracovat písemnou zprávu o celém postupu řešení.
Problémy budou voleny z různých oblastí, může jít o řešení her a hlavolamů (např. různé speciální varianty Sudoku), hledání vhodného rozvrhu, plánování směn, hledání vadné součástky v logickém obvodu apod.
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