Automated Reasonning Lecture Winter Semester 2026 / 2027
Organization
- Responsible: Mathias Fleury and Andre Schidler
- Mode: in-person lecture and exercises
- Language: English
- Monday (14-16) and Wednesday (10-12), in-person only
News
- October 10th: update lecture plan
- September 6th: Added expected oral exam dates
- September 6th: Added this page
Aim
This lecture is a generic introduction to automated reasonning beyond SAT solving (which is covered in depth in another lecture during summer – but it is not a requirement for this lecture).
It also shares some similarities with the “Decision Procedure” from Jochen Hoenicke (namely SMT solving) but has a wider scope, as we will also talk about MaxSAT, PB, proofs, and a bit of complexity.
Exam
There will be an oral exam. The exact dates are to be confirmed, but 18th and 26th of February are the current plane.
Plan 2026
This is a the plan from 2025.
As we reason in terms of weeks, we write only the start point of the week, you have to add 2 days or three to have the actual lecture day.
SAT
| Week start | Themes |
|---|---|
| 19. Oct. | Presentation |
| Logic | |
| 26. Oct | SAT |
| SAT Exercise | |
| 2. Nov | Proof checking |
| 9. Nov |
More expressive that SAT
| Week start | Themes |
|---|---|
| 16. Nov | User Propagator |
| 23. Nov | SMT |
| 30. Nov | SMT Proofs |
| 7. Dez | ASP |
Optimization
| Week start | Themes |
|---|---|
| 14. Dec | MaxSAT |
| 21. Dec | PBO, Exercises |
| Christmas | |
| 15. Jan | Proofs |
Week start 12 to 15: Different approaches
| Week start | Themes |
|---|---|
| 22. Jan | First order |
| 29. Jan | QBF, MC, ILP, ITP … |
| 2. Feb | Feedback + encoding sudoku SAT / AR / SMT |
ILIAS
Further details, current news and materials for the lecture will be made available on the ILIAS platform.