Monday, April 27, 2009
Humboldt-Universität zu Berlin
Institut für Informatik
Johann von Neumann-Haus
Rudower Chaussee 25
Raum 4.112
Lecture - 14:15
Abstract:
(joint work with Martin Dyer and Mark Jerrum)
The talk will introduce "partition functions", which arise in many
computational contexts, and will discuss the complexity of computing
them. It will explain what a "dichotomy theorem" is, and why we want
such theorems (essentially, we want them so that we can better
understand the boundary between the class of easy-to-compute functions
and the class of functions that cannot be efficiently computed).
The particular technical problem which forms the foundation for the
talk is the complexity of counting homomorphisms from an r-uniform
hypergraph G to a symmetric r-ary relation H. We give a dichotomy
theorem for r > 2, showing for which H this problem is in FP and for
which H it is #P-complete. Our dichotomy theorem extends to the case
in which the relation H is weighted, and the partition function to be
computed is the sum of the weights of the homomorphisms. This problem
is motivated by statistical physics, where it arises as computing the
partition function for particle models in which certain combinations
of r sites interact symmetrically.
Colloquium - 16:00
Abstract:
Modern SAT solvers have seen huge efficiency gains over the last decade. Being
well optimized implementations of the DPLL algorithm they are widely used in
many applications. Among these are, for example, microporocessor verification
and bounded model checking, which often require the solution of inputs with
hundreds of thousands of variables.
The fact that SAT solvers are indeed able to handle such situations apparently
conflicts with the well known intractability of the SAT problem. Recent
approaches by Beame, Kautz, Sabharwal and Bacchus, Hertel, Pitassi and Van
Gelder have tried to get a proof complexity theoretic account of this
phenomenon.
In a different direction we propose a more algorithmic view, relating
efficient solvability by a SAT solver to bounded width resolution. Among
other things this enables us to show that SAT solvers are able to handle CNF
formulas of bounded treewidth in polynomial time.
This is joint work with Albert Atserias and Johannes Fichte.