Satisfiability and Planning

Login to KOS for course enrollment Display time-table
Code Completion Credits Range
Pavel Surynek (guarantor)
Department of Applied Mathematics

The course offers a modern perspective on solving problems in artificial intelligence through satisfiability in logic (SAT) and finite domain constraint satisfaction problems (CSP). Satisfiability in logic, especially propositional logic, currently represents one of the most sophisticated approaches to state space search. We will discuss advanced techniques used in systematic solvers based on CDCL (conflict-driven clause learning), techniques for encoding pseudo-Boolean and cardinality constraints, symmetry-breaking techniques, satisfiability in first order logic theories, SAT modulo theories (SMT), and tractable cases where satisfiability has polynomial time complexity will also be discussed. We will emphasize the use of logic and satisfiability in the pivotal topic of symbolic artificial intelligence, namely in classical planning. In a closely related area of constraint satisfaction, we will focus on constraint propagation techniques, algorithms for maintaining consistencies such as arc or path consistency, filtering algorithms for global cardinality constraints, and problem modeling in CSP, especially planning. We give a unified view of CSP and SAT with strong emphasis on explanation of algorithmic principles.

Syllabus of lectures:
Syllabus of tutorials:

1. Complete algorithms for SAT, CDCL

2. Local incomplete algorithms, message passing algorithms, connection to statistical physics

3. Tractable cases of satisfiability with polynomial time complexity

4. Symmetry breaking techniques, cardinality constraints in SAT

5. Extensions: MaxSAT, QBF, pseudo-Boolean satisfiability

6. Satisfiability in first order logic and special theories, SAT modulo theories (SMT)

7. Classical planning as SAT

8. Constraint satisfaction problem (CSP), complete algorithms for CSP

9. Constraint propagation in CSP, domain filtering through consistency

10. Local and heuristic search algorithms (LDS - limited discrepancy search)

11. Global cardinality constraints and related effecient filtering algorithms

Study Objective:

The aim of the course is to provide a deep understanding of CSP and SAT techniques so that the graduate will be able to use these techniques independently and further develop them in their own research. The aim of the course is also to contribute to the education of top specialists in the field of symbolic artificial intelligence.

Study materials:

[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.

Time-table for winter semester 2022/2023:
Time-table is not available yet
Time-table for summer semester 2022/2023:
Time-table is not available yet
The course is a part of the following study plans:
Data valid to 2022-12-07
Aktualizace výše uvedených informací naleznete na adrese https://bilakniha.cvut.cz/en/predmet6219606.html