Automated Reasonning Lecture Winter Semester 2026 / 2027
Organization
- Responsible: Mathias Fleury and Andre Schidler
- Mode: in-person lecture and exercises
- Language: English
- TBA
News
- Adding information that oral exam
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 announced later.
Plan 2025
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 |
|---|---|
| 13. Oct. | Presentation |
| Logic | |
| 20. Oct | SAT |
| SAT Exercise | |
| 27. Oct. | Proof checking |
More expressive that SAT
| Week start | Themes |
|---|---|
| 3. Nov | User Propagator |
| 10. Nov | SMT |
| 17. Nov | SMT Proofs |
| 24. Nov | ASP |
Optimization
| Week start | Themes |
|---|---|
| 1. Dec | MaxSAT |
| 8. Dec | PBO, Exercises |
| 15. Dec | Proofs |
| Christmas |
Week start 12 to 15: Different approaches
| Week start | Themes |
|---|---|
| 5. Jan | First order |
| 12. Jan | QBF, MC, … |
| 19. Jan | ILP |
| 26. Jan | ASP |
| 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.