New upper bounds for the SAT/UNSAT threshold for shapes

Abstract

Phase transitions not only occur in physics but also in many problems in computer science. Among the problems from computer science, there are many NP-complete ones. An especially important problem is the satisfiability problem, SAT, for Boolean formulas. When phase transitions of SAT problems are studied, the corresponding formulas are usually restricted to conjunctive normal form, i.e., the formula is a set of clauses. K-SAT is the problem, where all clauses consists 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 KSAT problem with K > 2. There are only lower and upper bounds which are rigorously proven.<br />In this thesis, we consider formulas with more structure, namely the model of fixed balanced shapes introduced by Navarro and Voronkov in 2005.<br />They experimentally studied different shapes and provided first upper bounds for the critical value, i.e., the location where the phase transition occurs.<br />These upper bounds were obtained by using the first moment method (FMM).<br />We uniformly improve their upper bounds by a method which is based on locally maximal solutions. This method has been proposed by Creignou and Daude in 2007. Since this method requires a sensitivity polynomial as an input, we show how such polynomials can be computed for shapes, and how the upper bounds are obtained. We discuss the limitations of the method by comparing the upper bounds computed with the FMM with the upper bounds computed by the new method for shapes with increasing size or depth.