The course "Foundations of Artificial Intelligence V" introduces the foundations of constraint programming. The course covers constraint satisfaction and optimization problems as well as advanced algorithms that are used to solve these. It makes definitions relevant to constraint reasoning, introduces techniques used in CP, SAT and CP-SAT solvers and discusses the modelling of such problems in the constraint modelling language MiniZinc.

We discuss, in particular, how the techniques of Constraint Programming (CP) solvers and Satisfiability (SAT) solvers are joined in CP-SAT solvers to combine the advantages of both techniques. CP-SAT solvers are state of the art and can very quickly solve even extremely complicated problems. How to model problems so that these algorithms can solve them efficiently is also introduced on the example of the modelling language MiniZinc.

The course uses some of the theoretical background that was introduced in the Logic and Satisfiability course in this course series.

The thorough theoretical treatment of the definitions and algorithms is complemented with numerous examples.

The course is based on the textbook by Stuart Russell and Peter Norvig: Introduction to Artificial Intelligence, 3rd edition, 2012 or 4th edition, 2020. The 3rd edition is also available in German: Stuart Russell und Peter Norvig: Künstliche Intelligenz - Ein Moderner Ansatz, 3. aktualisierte Auflage, Pearson 2012. The course also uses material from the book by Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh: Handbook of Satisfiability, IOS Press, 2009, as well as the following two papers: Propagation via lazy clause generation, O. Ohrimenko, P. J. Stuckey, and M. Codish, Constraints 14.3 (2009): 357-391 and Lazy clause generation reengineered, T. Feydy and P. J. Stuckey, International Conference on Principles and Practice of Constraint Programming (2009).

The course is held in English language with German subtitles.

• Introduction to Constraint Satisfaction Problems (CSP)
• Reasoning techniques of Modern CSP Solver Types
  • Finite Domain Propagation (used by CP-Solvers)
  • Conflict Driven Clause Learning (used by SAT-Solvers)
  • Lazy Clause Generation (used by CP-SAT Solvers)
• Modelling of Constraint Satisfaction Problems

By the end of the course, you‘ll be able to

• formally talk about constraint satisfaction problems,
• understand Finite Domain Propagation and its use in CP-Solvers,
• understand how to extend the Davis-Putnam Logemann-Loveland Algorithm by clause learning to obtain the Conflict Driven Clause Learning Algorithm,
• understand how Lazy Clause Generation works and is used to combine the advantages of CP and SAT-Solvers in CP-SAT Solvers,
• model problems in MiniZinc and understand the challenges of good modelling

Foundations of Artificial Intelligence III: Logic and Satisfiability