Quantifizierte Boolesche Formeln: Komplexität und Solving (Vorlesung)

  Quantifizierte Boolesche Formeln: Komplexität und Solving
Verantwortlicher Benjamin Böhm
Leistungspunkte (ECTS credits) 4 SWS Vorlesung (6 LP)
geeignet für Masterstudierende
Zeiten Vorlesungstermine:
Di+Do 12-14 Uhr
im SR 3325

Erster Termin: 18.04.2023
Inhalte Einführung in die Beweiskomplexität und algorithmische Aspekte von quantifizierten Booleschen Formeln (QBF) als Erweiterung von SAT. Mögliche Themen:
  • Syntax und Semantik von QBFs
  • Beziehungen zur Aussagenlogik
  • 2-player-games, Gewinnstrategien
  • QBF-Beweissysteme, Erweiterungen von Resolution
  • Beispiele und Techniken für untere Schranken, QBF-„Härte“
  • Lösungsalgorithmen, insbesondere QCDCL als Erweiterung von CDCL
  • Expansions- und reduktionsbasierte Solver
Sprache Deutsch