Splnitelnost a plánování

Garant předmětu:

Pavel Surynek

Přednášející:

Cvičící:

Pavel Surynek

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 2024/2025:

Rozvrh není připraven

Rozvrh na letní semestr 2024/2025:

Rozvrh není připraven

Předmět je součástí následujících studijních plánů:

• Informatika (doktorská) (povinně volitelný předmět)
• Informatika (povinně volitelný předmět)