VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.

251-0491-00L 5 Credits
You're viewing possible stale or outdated data. Please check the latest semester for more up-to-date information.

Erfüllbarkeit logischer Formeln - Kombinatorik und Algorithmen

Lecturers & Examiners: Prof. em. Dr. Emo Welzl
VVZ CR n/a

Last Updated: 2026-02-05 14:53:04

Content

Satisfiability (SAT) is the problem of deciding whether a boolean formula in propositional logic has an assignment that evaluates to true. SAT occurs as a problem and is a tool in applications (e.g. Artificial Intelligence and circuit design) and it is considered a fundamental problem in theory, since many problems can be naturally reduced to it and it is the 'mother' of NP-complete problems. Therefore, it is widely investigated and has brought forward a rich body of methods and tools, both in theory and practice (including software packages tackling the problem). This course concentrates on the theoretical aspects of the problem (it is complementary to the SAT part of the parallel course Formal Verification by Armin Biere with emphasis on practical issues including tools and applications). We will treat basic combinatorial properties (employing the probabilistic method including a variant of the Lov´asz Local Lemma), recall a proof of the Cook-Levin Theorem of the NP-completeness of SAT, discuss and analyze several deterministic and randomized algorithms, briefly treat the threshold behavior of random formulas, and consider approximation algorithms and inapproximability results for the MAX-SAT problem (of satisfying as many clauses as possible in a formula in conjunctive normal form). In order to set the methods encountered into a broader context, we will deviate to the more general set-up of constraint satisfaction and to the problem of proper k-coloring of graphs.

General Information

Language
German
Frequency
Yearly recurring

Examination

Type
session examination
Mode
oral 30 minutes

Course Components

Type Title Time & Place Hours
lecture Erfüllbarkeit logischer Formeln - Kombinatorik und Algorithmen
  • Fri 10:15-12:00 (IFW B 42)
2 h weekly
exercise Erfüllbarkeit logischer Formeln - Kombinatorik und Algorithmen
  • Fri 13:15-14:00 (IFW B 42)
1 h weekly

Offered In