Decicion Procedures for Artificial Intelligence

This course is part of the IP Paris master's program in Computer Science and more precisely it is part of DataAI and CPS tracks.

The goal of this course is to present the main algorithms to solve Boolean logic formulas modeling of different problems such as path planning, task planning, diagnostics. In particular, the DPLL algorithm, and its extension CDCL, will be presented in a first part of the course to solve purely Boolean problems (satisfiability or unsatisfiability of logical formula). Then, extensions of logic formulas with terms coming from other theories (linear expressions in integers, real numbers, or non-linear expressions or recursive data structures), which are at the origin of SMT techniques (SAT Modulo Theories), will be presented. This second part will make the link between CDCL algorithms and classical constraint programming or mathematical programming algorithms. This teaching will show how complex decision problems can be solved effectively with exploratory techniques.