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 which 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 non-trivial distribution of graphs close to the critical threshold. For the restricted case of tree-like Parameterized Resolution, this result answers a question asked in [11] of understanding the Resolution complexity of this family of formulas. © 2011 Springer-Verlag.
Parameterized complexity of DPLL search procedures / Olaf, Beyersdorff; Galesi, Nicola; Lauria, Massimo. - STAMPA. - 6695 LNCS:(2011), pp. 5-18. (Intervento presentato al convegno 14th International Conference on Theory and Applications of Satisfiability Testing, SAT 2011 tenutosi a Ann Arbor, MI nel 19 June 2011 through 22 June 2011) [10.1007/978-3-642-21581-0_3].
Parameterized complexity of DPLL search procedures
GALESI, NICOLA;LAURIA, MASSIMO
2011
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 which 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 non-trivial distribution of graphs close to the critical threshold. For the restricted case of tree-like Parameterized Resolution, this result answers a question asked in [11] of understanding the Resolution complexity of this family of formulas. © 2011 Springer-Verlag.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
