Topics covered:
- SAT solving:
- Algorithms and advanced data structures
- Formula simplifications in SAT solvers
- Proofs produced by SAT solvers
- Satisfiability modulo Theories:
- Basics of DPLL(T) algorithm, concept of theory solvers
- Congruence closure algorithm for theory of equality with uninterpreted functions
- Other extensions of the satisfiability problem:
- Maximum Satisfiability
- Quantified Boolean Formulas
- Practical work with solvers of the presented problems
The content and organization of the course will be discussed in more details during an initial meeting (08.05.2023, 18:00, online)
where we will fix the format of the lecture and the lecture dates.
If you cannot attend this initial meeting, but you would like to participate, please send an email to katalin.fazekas@tuwien.ac.at.
First lecture (Vorbesprechung): 08.05.2023, 18:00, Zoom
ECTS breakdown
- 20h: 9 lectures a 2h + Q+A sessions for the reading + implemenation part
- 38h: reading a research paper (in teams of 2 students) + presenttation
- or implementing a new technique
- 16h:preparation for final exam
- 1h: final exam
Attention: The dates for the exams are from last year. They will be discussed in the first lecture "Vorbesprechung".
The course is planned to be in-person. However, if circumstances require, it will be changed to Distance Learning. In Distance Learning the lectures will be provided via ZOOM meetings.
Current literature like journal articles, articles from the Handbook of Satisfiability, etc. will be discussed during the lecture.
1) Propositional and predicate logic
a) Syntax, normal forms and normal form translations
b) Semantics, evaluation of a given formula with respect to a given interpretation, the concept of logical consequence (entailment) also under theories, Translation of validity, entailment, equivalence and satisfiablity problems into each other, proof procedures (beeing able to apply tableau, sequent systems or NK)
2) Ability to construct simple proofs
a) Induction proofs (for simple examples)
b) Simple proofs of run-time or space estimations (Example: Show that the time complexity of breadth first search with a fixed branching degree b and depth d is in O(b^d). I expect a formally correct proof including explanations (e.g., for the O-notation).
The previous knowledeg had been taught in the course "Theoretischer Informatik und
Logik" (TIL), "formalen Methoden der Informatik" (FMINF), "Algorithmen und Datenstrukturen" and
math lectures from the beginning of our bachelor studies. For a part of the knowledge about logic,
the slides of TIL and from the block Satisfiability (SAT) of FMINF (http://www.logic.at/lvas/fminf/) could be helpfull.