Proof Complexity - Interactive curriculae of TU Ilmenau

The interactive curriculae provide information on the degree programmes offered by the TU Ilmenau.

Please refer to the respective study and examination rules and regulations for the legally binding curricula (Annex Curriculum).

You can find all details on planned lectures and classes in the course catalogue.

Please note that this page is no longer updated. All modules and study plans from PO version 2021 onwards (Bachelor and Master study programs) are now available on the Campus Portal.

module properties Proof Complexity in degree program Master Informatik 2021
module number	201114
examination number	2200862
department	Department of Computer Science and Automation
ID of group	2242 (Algorithms)
module leader	Prof. Dr. Christoph Berkholz
term	winter term only
language	Deutsch
credit points	5
on-campus program (h)	34
self-study (h)	116
obligation	elective module
exam	oral examination performance, 30 minutes
details of the certificate
link to Moodle course	https://moodle.tu-ilmenau.de/course/view.php?id=1700
teacher	Prof. Berkholz
signup details for alternative examinations
maximum number of participants
previous knowledge and experience	Aussagenlogik, Komplexitätstheorie und lineare Algebra aus den Bachelor-Grundvorlesungen
learning outcome	Die Studierenden kennen grundlegende Resultate und Methoden der Beweiskomplexität und können Beweissysteme hinsichtlich ihrer Effizienz vergleichen. Sie wissen, wie Grenzen von Algorithmen mit Hilfe der Beweiskomplexität bewiesen werden können und sind in der Lage, die Vor- und Nachteile verschiedener algorithmischer Strategien zu beurteilen.
content	Die Beweiskomplexitätstheorie entstand aus der Frage heraus, ob die Klasse NP aller Entscheidungsprobleme mit Beweisen polynomieller Länge unter Komplement abgeschlossen ist: während bspw. jede erfüllende Belegung einer SAT-Instanz einen leicht zu überprüfenden Nachweis ihrer Erfüllbarkeit liefert, wird vermutet, dass es für unerfüllbare SAT-Instanzen im Allgemeinen keine kurzen Beweise ihrer Unerfüllbarkeit gibt. In der Beweiskomplexität wird die Frage, was sich effizient beweisen lässt, für konkrete Beweissysteme untersucht. Diese Systeme weisen häufig einen engen Zusammenhang zu Algorithmen für NP-schwere Probleme auf. Bekanntestes Beispiel ist der Resolutionskalkül, welcher die Grundlage für nahezu alle modernen SAT-Solver bildet. Die Lehrveranstaltung gibt eine Einführung in die Konzepte und Methoden der Beweiskomplexität und ihrer Anwendung in der Analyse von Algorithmen für NP-schwere Probleme. Neben dem Resolutionskalkül werden auch algebraische und semi-algebraische Beweisysteme und die entsprechenden Algorithmen vorgestellt. Beispielsweise: - Polynomial Calculus und Buchberger's Gröbnerbasis-Algorithmus - Cutting Planes und das Schnittebenenverfahren - Sum-of-Squares und semidefinite Optimierung
media of instruction and technical requirements for education and examination in case of online participation	Tafelvortrag, Beamerpräsentation, Skript, Übungsblätter
literature / references	Samuel R. Buss and Jakob Nordström: Proof Complexity and SAT Solving. In: Handbook of Satisfiability (2nd ed., 2021), Chapter 7. https://doi.org/10.3233/FAIA200990 Jan Krajícek: Proof Complexity. Cambridge University Press (2019). https://doi.org/10.1017/9781108242066
evaluation of teaching