Logo ČVUT
ČESKÉ VYSOKÉ UČENÍ TECHNICKÉ V PRAZE
STUDIJNÍ PLÁNY
2022/2023

Splnitelnost a plánování

Přihlášení do KOSu pro zápis předmětu Zobrazit rozvrh
Kód Zakončení Kredity Rozsah
PI-SPL ZK 4 3C
Přednášející:
Cvičící:
Pavel Surynek (gar.)
Předmět zajišťuje:
katedra aplikované matematiky
Anotace:

Předmět nabízí moderní pohled na řešení úloh v umělé inteligenci skrze splnitelnost v logice (SAT) a splňování omezení nad konečnými doménami (constraint satisfaction problem – CSP). Splnitelnost v logice zejména výrokové v současnosti představuje jeden z nejsofistikovanějších přístupů k prohledávání stavového prostoru. Probereme pokročilé techniky používané v systematických řešičích založených na CDCL (conflict-driven clause learning, konflikty řízené prohledávání s učením klauzulí), techniky kódování pseudo-booleovských podmínek a podmínek kardinality, využití symetrií, splnitelnost v teoriích logiky prvního řádu, SAT modulované teorie (satisfiability modulo theories - SMT) a zmíníme též speciální případy, kdy má splnitelnost polynomiální časovou složitost. Budeme klást důraz na využití logiky a splnitelnosti ve stěžejní úloze symbolické umělé inteligence, a sice v klasickém plánování. V úzce související oblasti problémů splňování omezení se zaměříme na techniky propagace podmínek, algoritmy udržování konzistence jako je například hranová nebo konzistence po cestě, filtrační algoritmy pro globální podmínky kardinality a na otázky modelování úloh v CSP zejména úlohy plánování. Podáme jednotný pohled na CSP a SAT s důrazem na vysvětlení algoritmických principů.

Požadavky:
Osnova přednášek:
Osnova cvičení:

1. Úplné algoritmy pro SAT, CDCL

2. Lokální neúplné algoritmy, posílání zpráv, souvislost se statistickou fyzikou

3. Speciální případy splnitelnosti s polynomiální časovou složitostí

4. Symetrie a splnitelnost, podmínky kardinality v SATu

5. Rozšíření: MaxSAT, QBF, pseudo-booleovská splnitelnost

6. Splnitelnost v logice prvního řádu a speciálních teoriích, SAT modulované teorie (SMT)

7. Klasické plánování jako SAT

8. Problém splňování omezení (CSP), úplné algoritmy pro CSP

9. Propagace podmínek v CSP, filtrace domén skrze konzistence

10. lokální a heuristické algoritmy (LDS – limited discrepancy search) splňování omezení

11. Globální podmínky kardinality a jejich efektivní filtrační algoritmy

12. Modelování úloh v CSP, CSP vs. SAT, plánování jako CSP

13. Optimalizace v CSP, hierarchie podmínek, měkké podmínky, složitost

Cíle studia:

Cílem studia předmětu je zprostředkovat hluboké pochopení technik splnitelnosti pro CSP a SAT tak, aby absolvent byl schopen samostatně tyto techniky používat a dále je rozvíjet v rámci vlastního výzkumu. Předmět má za cíl přispět k výchově špičkových odborníků v oblasti symbolické umělé inteligence.

Studijní materiály:

[1] Biere, A., Heule, M., Van Maaren, H., Walsh, T.: Handbook of Satisfiability. IOS Press, 2009.

[2] Dechter, R.: Constraint Processing. Morgan Kaufmann, 2003.

[3] Ghallab, M, Nau, D., Traverso, P.: Automated Planning: theory & practice. Morgan Kaufmann, 2004.

Poznámka:
Rozvrh na zimní semestr 2022/2023:
Rozvrh není připraven
Rozvrh na letní semestr 2022/2023:
Rozvrh není připraven
Předmět je součástí následujících studijních plánů:
Platnost dat k 7. 10. 2022
Aktualizace výše uvedených informací naleznete na adrese https://bilakniha.cvut.cz/cs/predmet6219606.html