Paper Info
Title
Parameterized Complexity of DPLL Search Procedures
Abstract
We study the performance of DPLL algorithms on parameterized problems. In particular, we investigate how difficult it is to decide whether small solutions exist for satisfiability and other combinatorial problems. For this purpose we develop a Prover-Delayer game that models the running time of DPLL procedures and we establish an information-theoretic method to obtain lower bounds to the running time of parameterized DPLL procedures. We illustrate this technique by showing lower bounds to the parameterized pigeonhole principle and to the ordering principle. As our main application we study the DPLL procedure for the problem of deciding whether a graph has a small clique. We show that proving the absence of a k-clique requires nΩ(k) steps for a nontrivial distribution of graphs close to the critical threshold. For the restricted case of tree-like Parameterized Resolution, this result answers a question asked by Beyersdorff et al. [2012] of understanding the Resolution complexity of this family of formulas.
Year
DOI
Venue
2011
10.1007/978-3-642-21581-0_3
ACM Transactions on Computational Logic
Keywords
Field
DocType
small clique,resolution complexity,dpll search procedure,prover-delayer game,parameterized pigeonhole principle,dpll procedure,parameterized problem,parameterized dpll procedure,small solution,dpll algorithm,parameterized complexity,lower bound
Graph,Discrete mathematics,Parameterized complexity,Combinatorics,Clique,Computer science,Critical threshold,Satisfiability,DPLL algorithm,Pigeonhole principle
Conference
Volume
ISSN
Citations 
6695
0302-9743
16
PageRank 
References 
Authors
0.63
33
3
Name
Order
Citations
PageRank
Olaf Beyersdorff122330.33
Nicola Galesi236728.05
Massimo Lauria312214.73