Summary: The course will cover the basics of Boolean Reasoning, presenting the techniques at the heart of the current state-of-the-art propositional solvers based on learning. Then, it will be shows how these algorithms can be extended in order to deal with more complex formalisms such as quantified boolean formulas and/or difference logic. The applications of the presented algorithms for solving symbolic reachability problems (such as those arising in automated planning or model checking) will be presented and discussed.
Prerequisites: Some background knowledge of propositional logic.
