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
