Automated Planning and Reasoning

Course guarantor:

Lecturer:

Tutor:

Supervisor:

Department of Computer Science

Synopsis:

Requirements:

Syllabus of lectures:

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)

Syllabus of tutorials:

Study Objective:

Study materials:

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.

Note:

Further information:

No time-table has been prepared for this course

The course is a part of the following study plans:

• Open Informatics - Artificial Intelligence (PS)