### Content

The elective module Constraint Solving provides an introduction into the theory and practice of constraint solving. The following topics will be discussed:

- propositional logic (SAT and Max-SAT)
- Boolean combination of constraints, satisfiability modulo theories (SMT)
- constraints about equality logic and uninterpreted functions (EUF)
- linear arithmetic constraints (LIA and LRA), linear programming
- constraints involving arrays
- constraints using quantifiers (QBF)

week | date | topics | slides | exercises |
---|---|---|---|---|

01 | 07.10 & 12.10 | SAT basics | pdf (x1, x4) | |

02 | 19.10 | Conflict Graphs, NP completeness | pdf (x1, x4) | |

03 | 21.10 & 28.10 | NP completeness of Shakashaka, MaxSAT | pdf (x1, x4) | |

04 | 04.11 & 09.11 | FO-Theories, SMT, DPLL(T) | pdf (x1, x4) | |

05 | 11.11 & 16.11 | Equality Logic, EUF | pdf (x1, x4) | |

06 | 18.11 & 23.11 | Difference Logic, Simplex | pdf (x1, x4) | |

07 | 25.11 & 30.11 | Farkas' Lemma, Complexity and Incrementality of Simplex | pdf (x1, x4) | |

08 | 02.12 & 07.12 | Branch-and-Bound, Small Model Property of LIA | pdf (x1, x4) | |

09 | 09.12 & 14.12 | Bit-Vector Arithmetic | ||

10 | 16.12 & 11.01 | Nelson-Oppen, QBF, PSPACE completeness | ||

11 | 13.01 & 18.01 | Ferrante-Rackoff, Cooper's Method | ||

12 | 20.01 & 25.02 | Arrays | ||

13 | 27.01 & 01.02 | Q&A, Repeat for exam | ||

14 | 03.02 | 1st exam |

### Further Material

### Literature

The course is partly based on the following books:-
Daniel Kroenig and Ofer Strichman

Decision Procedures — An Algorithmic Point of View (second edition)

Springer, 2016 -
Aaron Bradley and Zohar Manna

The Calculus of Computation — Decision Procedures with Applications to Verification

Springer, 2007

Slides and exercises are available from this page. Recordings of the lectures (if lectures turn virtual) will be available from the OLAT course of the lecture. Solutions to exercises will be made available via the OLAT course of the proseminar.