Monday, April 27, 2009
Humboldt-Universität zu Berlin
Institut für Informatik
Johann von Neumann-Haus
Rudower Chaussee 25
Lecture - 14:15
(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
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.