TU Wien:SAT Algorithms Applications and Extensions VU (Fazekas)

Daten

Vortragende	Katalin Fazekas
ECTS	6,0
Letzte Abhaltung	2026S
Sprache	English
Mattermost	sat-algorithms-applications-and-extensions • Register • Mattermost-Infos
Links	tiss:192186, eLearning, Homepage

Zuordnungen

Masterstudium Logic and Computation	Modul SAT Algorithms, Applications and Extensions * (Gebundenes Wahlfach)
Masterstudium Software Engineering & Internet Computing (veraltet)	Modul SAT Algorithms, Applications and Extensions * (Gebundenes Wahlfach)
Masterstudium Technische Informatik	Modul * Modul Wahlmodul Computer-Aided Verification (Gebundenes Wahlfach)

Inhalt

Sat solving techniques such as DP, DPLL, CDCL. Decision Heurisitcs, other implementation tricks. Smt solving with lazy and tight integration and the ipasir-up interface. MaxSat and techniques to solve it efficiently. Qbf solving.

Ablauf

Weekly lectures with a mini-test in the first 5 minutes and 4 projects during the hole semester. One final exam at the end of the semester.

The material is covered in the order as it is listed in the Inhalt section. The first half is about sat solving the rest about different extensions.

Benötigte/Empfehlenswerte Vorkenntnisse

some knowledge about propositional is helpful but not required. For the programming projects it is helpful be able to implement small projects in python, rust or c++.

Vortrag

Very interactive and very good. Questions are actively encouraged and asked by the lecturer to the students too.

The mini-tests are very easy and basically free points.

Übungen

This is the most time consuming part of the course.

The first project is the smallest. You have to automatically encode a 3-colorability instance into a sat problem.

The second project requires to implement a DPLL sat solver with exhaustive propagation. The general structure of the solver is explained nicely in the lecture.

The third project is an extension of the second. Starting from a DPLL sat solver a CDCL sat solver with resets and clause database reduction should be implemented. This project is less constrained than the second as one can decide which methods (that where presented in the lecture) one wants implement.

The forth project is to implement a smt solver using an existing sat solver. The only theory the theory solver must use is the theory of equality (without functions). One has to use the IPASIR-UP interface.

Prüfung, Benotung

The exam is very fair as the exam problems are pretty much a subset of the exercise problems.

Dauer der Zeugnisausstellung

noch offen

Zeitaufwand

noch offen

Unterlagen

noch offen

Tipps

noch offen

Highlights / Lob

Very interactive lecture. Very good student-lecturer relation (professor Fazekas knows the students by their first name).

Verbesserungsvorschläge / Kritik

noch offen

Materialien

Neues Material hinzufügen

2

• 2026S Cheatsheet.pdf (details)