Colloquium on Complexity and Logic
On the occasion of the retirement of Professor Martin Mundhenk
- Date: Friday, June 21, 2024
- Place: Haus auf der Mauer, Johannisplatz 26, 07743 Jena
- Registration: https://indico.rz.uni-jena.de/e/colloquium
Program Schedule:
đ 13:00 - 13:30
Arrival and Welcome
đ 13:30 - 14:00
The good, the bad, and the ugly days of a long-lasting friendship
Speaker: Heribert Vollmer (Hannover)
Abstract: We present the results of a year-long collaboration between the Universities of Jena and Hannover on the complexity of different temporal logics. A key tool in this approach is the use of Postâs lattice of all closed classes of Boolean functions, which allows us to conduct a comprehensive study of the complexity of satisfiability and model checking for logics such as LTL, CTL, and CTL*.
đ 14:00 - 14:40
On the Satisfaction Probability of k-CNF Formulas
Speaker: Till Tantau (LĂŒbeck)
Abstract: The satisfaction probability Pr[Ï] of a propositional formula Ï is the likelihood that a random assignment makes the formula true. These probabilities can take any dyadic value (a number of the form a/2^b for integers a and b) from the interval [0,1], but what happens when we only consider kCNF formula for a fixed k? The Spectral Well-Ordering Theorem states that then, somewhat surprisingly, the spectrum of values that Pr[Ï] can take is well-ordered by the greater-than relation. Equivalently, there are âholes in the spectrum everywhereâ. A direct consequence of this is that while MAJ-SAT is a well-known PP-complete problem, MAJ-kSAT is a very easy problem for all k. A corollary of this, in turn, the following cute result: Telling for a 3CNF formula Ï whether exactly half of all assignments are satisfying (that is, telling whether Pr[Ï] = 1/2 holds) is NL-complete.
đ 14:40 - 15:10
Break
đ 15:10 - 15:50
Persönliche Erfahrungen mit SAT-Solvern: Theorie und Praxis
Speaker: Uwe Schöning (Ulm)
Abstract: Vor Jahren habe ich einen SAT-Solver (Entscheidungsalgorithmus fĂŒr das aussagenlogische ErfĂŒllbarkeitsproblem) nach dem SLS (stochastic local search) - Prinzip konzipiert, der zur damaligen Zeit die beste theoretisch nachweisbare worst-case Laufzeit hatte. Es wird eine vereinfachte Analyse vorgestellt, die von jedem (?) Abiturienten nachvollziehbar sein sollte. Experimente mit zufĂ€llig generierten Formeln zeigten jedoch, dass dieser Solver bei der jĂ€hrlich stattfindenden SAT-Competition keineswegs gut abschnitten hĂ€tte. Anstatt die Auswahl der nĂ€chsten Flip-Variablen unter stochastischer Gleichverteilung durchzufĂŒhren, verwendeten wir eine "Softmax"-Funktion, um die betreffenden Auswahl-Wahrscheinlichkeiten festzulegen. Solcherart mit Zufallsformeln "trainiert" hat dieser modifizierte Solver die damalige SAT-Competition gewonnen.
đ 15:50 - 16:30
Spiele auf Graphen und die KomplexitÀt von Resolution
Speaker: Jacobo Toran (Ulm)
Abstract: Das ErfĂŒllbarkeitsproblem von aussagenlogischen Formeln ist eine zentrale Frage der Informatik, sowohl in theoretischer als auch in praktischer Hinsicht. Einerseits ist dieses Problem NP-vollstĂ€ndig und daher sehr schwierig aus algorithmischer Sicht zu lösen. Anderseits können moderne Programme Instanzformeln mit buchstĂ€blich Tausenden von Booleschen Variablen lösen. Resolution ist das bekannteste Beweissystem um zu zeigen, dass eine aussagenlogische Formel unerfĂŒllbar ist. Oft ist die Analyse der KomplexitĂ€t solcher Beweise sehr komplex. In diesem Vortrag werde ich einige bekannte Spiele auf Graphen anwenden, um die KomplexitĂ€t von Resolutionsbeweisen fĂŒr konkrete Formelfamilien zu untersuchen.
đ 16:30 - 17:10
Farewell to Martin Mundhenk
đ Following
Get-together with snacks