Title: New upper bounds for the SAT/UNSAT threshold for shapes
Language: English
Authors: Santillán Rodríguez, Rocío 
Qualification level: Diploma
Keywords: Phasenuebergang; Erfuellbarkeit; obere Schranke; random SAT
phase transition; satisfiability; upper bound; random SAT
Advisor: Egly, Uwe
Issue Date: 2007
Number of Pages: 51
Qualification level: Diploma
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.
In this thesis, we consider formulas with more structure, namely the model of fixed balanced shapes introduced by Navarro and Voronkov in 2005.
They experimentally studied different shapes and provided first upper bounds for the critical value, i.e., the location where the phase transition occurs.
These upper bounds were obtained by using the first moment method (FMM).
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.
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-21135
Library ID: AC05034964
Organisation: E184 - Institut für Informationssysteme 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

File Description SizeFormat
New upper bounds for the SATUNSAT threshold for shapes.pdf488.44 kBAdobe PDFThumbnail
Show full item record

Page view(s)

checked on Feb 18, 2021


checked on Feb 18, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.