Automated Reasonning Lecture Winter Semester 2025 / 2026
Organization
- Responsible: Mathias Fleury and Andre Schidler
- Mode: in-person lecture and exercises
- Language: English
- Wednesday (8 to 10) and Thursdays (2 to 4), SR 00 034
News
Lecture on Wednesday Morning 8am to 10am and the exercise class on Thursday 2pm to 4pm. Both of them will be in the SR 00 034 (G.-Köhler-Allee 051)
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.
This semester you might also be interested in the SMT Seminar that will go into more details into SMT solving (like shiny theories).
Plan 2025
This is a rough plan. It might change.
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 | |
| 26. Jan | |
| 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.