184.090 SAT Solving This course is in all assigned curricula part of the STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_21",{id:"j_id_21",showEffect:"fade",hideEffect:"fade",target:"isAllSteop"});});This course is in at least 1 assigned curriculum part of the STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_23",{id:"j_id_23",showEffect:"fade",hideEffect:"fade",target:"isAnySteop"});}); 2024S 2023S 2022S 2021S 2019S 2018S 2017S 2016S 2015S 2014S 2013S 2012S 2011S 2010S 2009S 2008S 2007S 2006S 2005S 2004S 2003S 2002S 2001S 2000S 1999W 1999S 1998W

2018S, VU, 2.0h, 3.0EC

Properties

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

Aim of course

• Knowledge about theory and proof procedures for propositional logic and quantified propositional logic
• Knowledge about applications like planning
• Practical knowledge about proof systems (like minisat or depQBF)

Didactic Procedure

• Lecture
• Processing of simple exercises by students (e.g., complete a proof presented in the lecture).
• Preparation as home work or in small working groups (for 10 to 15 minutes) during the lecture
• Short presentation and discussion of solutions and results.
• Short oral presentation of relevant papers including a short written review.

Subject of course

• Syntax, semantic, etc. for the mentioned logics proof
• Procedures for these logics especially for quantified Boolean formulas
• New developments like, e.g., solver in non-normal form, circuits, certificates and their extraction from proofs etc.
• Practical work with selected provers and implementations (e.g., preprocessors).
• A more detailed presentation of the content of the summer term will be presented in the first lecture

ECTS breakdown

• 18h: 9 lectures a 2h
• 15h: 3 ex sheets a 5 ex; including preparation of a solution in pdf)
•  6h: ex presentation
•  8h: reading a research paper (in teams of 2 students)
• 12h: preparation of paper presentation
•   7h: presentation (10 teams, 3 presentations in a 2h slot)
•   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"

Course dates

DayTimeDateLocationDescription
Mon12:00 - 14:0021.05.2018 meeting room Menger HF0311 (at the institute)SAT Solving und Erweiterungen
Mon16:30 - 18:3021.05.2018 meeting room Menger HF0311 (at the institute)SAT Solving und Erweiterungen
Mon12:00 - 14:0028.05.2018 meeting room Menger HF0311 (at the institute)SAT Solving und Erweiterungen
Fri13:00 - 15:0001.06.2018 Meetingroom Menger (HF0311) - at the instituteSAT Solving und Erweiterungen
Mon13:00 - 17:0004.06.2018 Meetingroom Menger (HF0311) - at the instituteSAT Solving und Erweiterungen
Tue10:00 - 12:0005.06.2018 Meetingroom Menger (HF0311) - at the instituteSAT Solving und Erweiterungen

written and oral

Not necessary

Curricula

Study CodeObligationSemesterPrecon.Info
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.

English