184.090 SAT Solving
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2024S, VU, 2.0h, 3.0EC
TUWEL

Course evaluation

Properties

  • Semester hours: 2.0
  • Credits: 3.0
  • Type: VU Lecture and Exercise
  • Format: Hybrid

Learning outcomes

After successful completion of the course, students are able to...

  •     understand and compare many automated reasoning techniques
  •     understand, use and modify advanced data structures and algorithms of modern SAT solvers
  •     select and use relevant techniques and methods to design SAT-based solving algorithms for new problems

Subject of course

Topics covered:

  • SAT solving:
    • Algorithms and advanced data structures
    • Formula simplifications in SAT solvers
    • Proofs produced by SAT solvers
    • Incremental Reasoning
  • Extensions of the satisfiability problem:
    • Maximum Satisfiability
    • Quantified Boolean Formulas
    • Satisfiability modulo Theories
  • Practical work with solvers of the presented problems

The content and organisation of the course will be discussed in more details during an initial meeting (5th March, 18:00, Seminarraum FAV 01 A)
where we will fix the format of the lecture and decide on which day and in which timeslot it will take place.

If you cannot attend this initial meeting, but you would like to participate, please send an email to katalin.fazekas@tuwien.ac.at.


Teaching methods

  • Lecture
  • Mandatory exercises
  • Supporting Q+A sessions
  • Practical work with solvers

Mode of examination

Oral

Additional information

First lecture (Vorbesprechung): 5th March, 18:00,  Seminarraum FAV 01 A

ECTS breakdown

  • 22h: 10 lectures a 2h + Q+A sessions for the reading + implemenation part
  • 15h: 3 ex sheets; (including preparation of a solution in pdf)
  • 3h: ex presentation
  • 20h: reading a research paper or implementing a technique +
            preparing presentation
  • 6h: paper/project presentation
  • 8h: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.

Lecturers

Institute

Course dates

DayTimeDateLocationDescription
Tue18:00 - 20:0005.03.2024Seminarraum FAV 01 A (Seminarraum 183/2) Vorbesprechung
Fri12:00 - 14:0015.03.2024 - 24.05.2024Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fri13:00 - 15:0019.04.2024Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fri13:00 - 15:0007.06.2024 - 14.06.2024Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fri13:00 - 15:0021.06.2024Seminarraum FAV EG B (Seminarraum von Neumann) Lecture
SAT Solving - Single appointments
DayDateTimeLocationDescription
Tue05.03.202418:00 - 20:00Seminarraum FAV 01 A (Seminarraum 183/2) Vorbesprechung
Fri15.03.202412:00 - 14:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fri22.03.202412:00 - 14:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fri12.04.202412:00 - 14:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fri19.04.202413:00 - 15:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fri03.05.202412:00 - 14:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fri17.05.202412:00 - 14:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fri24.05.202412:00 - 14:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fri07.06.202413:00 - 15:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fri14.06.202413:00 - 15:00Seminarraum FAV 01 C (Seminarraum 188/2) Lecture
Fri21.06.202413:00 - 15:00Seminarraum FAV EG B (Seminarraum von Neumann) Lecture

Examination modalities

Oral exam

Course registration

Begin End Deregistration end
08.02.2024 15:00 08.04.2024 23:00

Curricula

Study CodeObligationSemesterPrecon.Info
066 504 Master programme Embedded Systems Not specified
066 931 Logic and Computation Mandatory elective
066 937 Software Engineering & Internet Computing Mandatory elective
066 938 Computer Engineering Mandatory elective
881 Computer Sciences Mandatory elective

Literature

Current literature like journal articles, articles from the Handbook of Satisfiability, etc. will be discussed during the lecture.

Previous knowledge

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.

Miscellaneous

Language

English