Automated Planning and Reasoning
Semestr: Summer
Range: 2P+2C
Completion:
Credits: 6
Programme type: Master
Study form: Fulltime
Course language: English
Summary:
Keywords:
Course syllabus:
1. Introduction and motivation - propositional logic and various representations (CNFs, circuits, and BDDs)
2. SAT - basic encodings and search (DPLL algorithm and resolution)
3. SAT - CDCL
4. SAT - advanced encodings, BMC, introduction to SMT
5. SMT - lazy solving, congruence closure algorithm, theory combination
6. Problems beyond the class NP in logic and probabilistic inference (NP, PP, NP^PP, PP^PP, etc.).
7. Tractable Logic Circuits I.
8. Tractable Logic Circuits II.
9. From tractable logic circuits to tractable models of probability distributions.
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. Reserve (Proof assistants)
Seminar syllabus:
Literature:
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.