Automatizované plánování a uvažování

Garant předmětu:

Přednášející:

Cvičící:

Předmět zajišťuje:

katedra počítačů

Anotace:

Požadavky:

Osnova přednášek:

1. Úvod and motivace - výroková logika a různé reprezentace (KNF, obvody, binární rozhodovací diagramy) /

Introduction and motivation - propositional logic and various representations (CNFs, circuits, and BDDs)

2. SAT - základní kódování a vyhledávání (DPLL algoritmus a rezoluce) / SAT - basic encodings and search (DPLL

algorithm and resolution)

3. SAT - CDCL / SAT - CDCL

4. SAT - pokročilá kódování, BMC, úvod do SMT / SAT - advanced encodings, BMC, introduction to SMT

5. SMT - líné kódování, kongruenční uzávěr, kombinace teorií / SMT - lazy solving, congruence closure algorithm,

theory combination

6. Problémy za třídou složitosti NP v logice a pravděpodobnostním vyvozování (NP, PP, NP^PP, PP^PP, etc.).

7. Výpočetně efektivní logické obvody I (Tractable Logic Circuits I).

8. Výpočetně efektivní logické obvody II (Tractable Logic Circuits II)

9. Od výpočetně efektivních logických obvodů k výpočetně efektivním modelům pravděpodobnostních distribucí.

10. Introduction to automated planning, state space representations PDDL, STRIPS, FDR

11. Heuristic search algorithms GBFS, A*, Weighted A*

12. Delete relaxation heuristics hmax, hadd, hff

13. Symbolic planning

14. Rezerva (Důkazoví asistenti) / Reserve (Proof assistants)

Osnova cvičení:

Cíle studia:

Studijní materiály:

Kroening, D., & Strichman, O. (2016). Decision Procedures: An Algorithmic Point of View (2nd ed.). Springer.

https://doi.org/10.1007/978-3-662-50497-0 (freely accessible from CTU)

Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.). (2021). Handbook of satisfiability (2nd ed.). IOS Press.

Avigad, J., Heule, M. J. H., & Nawrocki, W. (2025). Logic and Mechanized Reasoning (Release 0.1).

https://avigad.github.io/lamr

Malik Ghallab,Dana Nau,Paolo Traverso: Automated Planning and Acting, Cambridge University Press, 2016.

Poznámka:

Další informace:

Pro tento předmět se rozvrh nepřipravuje

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