CAGT Seminar: Rocio Santillan: Phase transitions insatisfiability
2007.11.27 |
| Date | Tue Dec 11 |
| Time | 14:15 — 15:15 |
| Location | DI-Turing-014 |
Title: Phase transitions in satisfiability
Speaker: Rocio Santillan
Time: Tue Dec 11th 2007 14:15-15:15
Location: Turing-014
Abstract:
Phase transitions not only occur in physics but also in many problems in computer science. An especially important problem is the satisfiability problem, SAT, for Boolean formulas. K-SAT is the problem, where the formulas are restricted to clauses consisting of exactly K literals. When the density of clauses (i.e., the ratio between the number of clauses and the number of variables) is increased in random K-SAT problems, there is an abrupt change in the probability from being satisfiable to being unsatisfiable. Numerous experimental results are available, but the exact location of the phase transition is not known for the random K-SAT problem with K > 2. There are only lower and upper bounds which are rigorously proven.
We consider formulas with more structure, the model of fixed balanced shapes introduced by Navarro and Voronkov in 2005. They provided first upper bounds for the location of the critical value, i.e., where the phase transition occurs. These upper bounds were obtained by using the first moment method (FMM).
In this talk, we present how toimprove the upper bounds by a method which is based on locally maximal solutions. This method has been proposed by Creignou and Daudé in 2007. Since this method requires a sensitivity polynomial as an input, we show how such polynomials can be computed for shapes in general.