Algorithms, Structure, Randomness

Learn- & Workshop 2006

"Algorithms for the SAT-Problem"

Featured speakers: Riccardo Zecchina und Eugene Goldberg

Humboldt-Universität zu Berlin, October 27th-29th 2006

• Schedule
• Abstracts
• Pictures
• Contact

Schedule:

Program as PDF-Document
All lectures will be held in

 Erwin Schrödinger-Zentrum, HU Berlin
 Rudower Chaussee 26,
 12489 Berlin

in the rooms 1.303, 1.305.
(for information of arrival look at Address of ESZ or the city map.)

---

Abstracts:

Riccardo Zecchina

Statistical Physics of Constraint Satisfaction Networks

In the recent years there has been an emergence of converging concepts and methods in Information Theory, Combinatorial Optimization and Statistical Physics. In these lectures we shall provide a brief introduction to Statistical Physics, relying mainly on its combinatorial foundation. The application of statistical physics techniques to random Constraint Satisfaction problems will be discussed in some detail together with some rigorous probabilistic results. Finally, we shall discuss the algorithmic outcomes of the physical methods, with particular focus on message-passing algorithms and on their applications.
The level of the lectures will be introductory, aiming at communicating in an intuitive way the main ideas behind the statistical physics approach to random combinatorial optimization problems (e.g. K-SAT) to mathematicians and computer scientists.

1. Introduction to statistical physics:
   combinatorial interpretation
   Phase transition in the Ising problem
   Phase transitions in spin glasses
2. Statistical Physics of random Constraint Satisfaction Problems
   random k-xor-sat phase diagram and its rigorous derivation
   statistical mechanics of random k-sat
   the phase diagram from the cavity method
   clustering of solutions
   rigorous results on clustering
3. Message-passing algorithms
   From the cavity method to Survey Propagation (SP)
   Belief Propagation (BP) versus SP
   Some applications
   Perspectives and Open Problems

Eugene Goldberg

Practical SAT solving: achievements, problems and opportunities

This series of lectures consists of 3 parts.

1. In the first (and the largest) part, we will discuss the current state-of-the-art solvers for the propositional satisfiability problem (SAT). I will describe the interior of modern resolution based SAT-solvers that have been so successful lately in practical applications and explain the reasons for this success.
2. In the second part, we will discuss the importance of providing "external" information for efficient SAT-solving by the example of CNF formulas describing equivalence checking of combinational circuits with a "common specification" of fixed "granularity". For the formulas of this class there are linear size proofs of unsatisfiability in the resolution proof system. However, most likely, there is no efficient deterministic algorithm for finding those proofs. So these formulas cannot be solved efficiently by a "black box" SAT-solver.
3. In the third part, I will describe a method of solving SAT by computing a stable set of points. The main attraction of this method is that it allows one to take into account structural properties of the formulas (e.g. symmetry) and so make a SAT-solver more "intelligent".

Pictures:

Contact:

Dr. Amin Coja-Oghlan

Postal address
Johann von Neumann-Haus
Humboldt-Universität zu Berlin
Institut für Informatik
Rudower Chaussee 25
12489 Berlin


Tel.   : (+49 30) 2093 3803
Fax    : (+49 30) 2093 3191
e-mail : coja@informatik.hu-berlin.de

Prof. Dr. Stephan Kreutzer

Postal address
Johann von Neumann-Haus
Humboldt-Universität zu Berlin
Institut für Informatik
Rudower Chaussee 25
12489 Berlin


Tel.   : (+49 30) 2093 3075
Fax    : (+49 30) 2093 3081
e-mail : kreutzer@informatik.hu-berlin.de

---

last modified 11/29/06 (alkox-www)