The concept of backdoor was introduced to try to explain the good performances achieved on real world SAT instances by solvers. A backdoor is simply a set of variables that, once decided, makes the rest of the problem simple (i.e. polynomial-time).

In this thesis I provide a comprehensive overview on the state of the art of backdoors for SAT. Moreover, I study the relation between backdoors and parameterized complexity. In order to do so, I consider the problem of finding a smallest strong Horn-backdoor and I study it by means of the parameterized version of Vertex Cover.

Presentations

• Master defense (October 2011)
• Introduction to parameterized complexity (July 2011)
• Introduction to backdoors (June 2011)

Software

During the development of my thesis I developed a series of tools to allow the study of strong Horn-backdoors.

HornVCBuilder.jar By issuing: java -jar HornVCBuilder.jar filename.cnf <emph> it is possible to generate the graph associated with the strong Horn-backdoor detection problem of the instance filename.cnf.

Additional options are available to compute anti-horn, try to reduce the output graph, skip empty clauses etc. The CNF file is expected to be in DIMACS format.

FPT Tools: fptTools.jar, SVN (Assembla). A longer introduction to these tools is provided on the SVN repository. The jar file runs the HdK kernelization and the bounded search described in the thesis. The main class of this jar is org.gario.marco.fpttools.demo.Solver. This class is meant to be used to experiment with different types of algorithms. By using the options -k and -s it is possible to define a different kernelization or search algorithm.

To perform a search without kernelization use -k org.gario.marco.fpttools.EmptyKern. To perform the kernelization only, call the main of the class org.gario.marco.fpttools.demo.Kernelizer

SATdb (python). The SATdb includes the dataset with the information about the instances. Run python satdb.py to get the usage.

Datasets

Here you can find the datasets used for the experimental part. These datasets do not include the instances by themselves, but only meta-data/features of these instances.

General information about the instances. This dataset was obtained by issuing the command:

$ satdb -csv join VariableCnt ClauseCnt isCrafted isRandom \
                    isIndustrial %VarToClause NegativeLiteralCnt \
                    PositiveLiteralCnt avgClauseSize minClauseSize \
                    maxClauseSize devClauseSize is2SAT isAntiHorn \
                    isHorn \
                    edges vertices

The last two properties (vertices and edges) refer to the graph obtained from the instance to solve strong Horn-backdoor detection by means of Vertex Cover.

Upper- and Lower-bounds obtained by COVER, FPT algorithms and Cryptominisat:

$ satdb -csv join mvc-ub mvc-lb

Runtime of COVER with the fast configuration:

$ satdb -csv getProperty localsearchSQ-avg | cut -d',' -f1,3

Complete database (to use with SATdb) and Hard Unsatisfiable SAT instances from Vertex Cover (7.5MB)