Colloquium on Complexity and Logic

On the occasion of the retirement of Professor Martin Mundhenk


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