Hard satisfiable instances for DPLL algorithms and other weak models of computation
Mikhail (Misha) Alekhnovich, Institute for Advanced Study
March4, 2005

Abstract

DPLL (for Davis, Putnam, Logemann, and Loveland) algorithms form the largest family of contemporary algorithms for SAT (the propositional satisfiability problem) and are widely used in applications. While the behavior of DPLL algorithms on unsatisfiable formulas has been extensively investigated (by studying the refutation size in Resolution proof system), little research was done towards proving lower bounds on satisfiable instances. We fill this gap by constructing satisfiable formulas which are provably difficult for a wide class of DPLL algorithms.

In the second part of the talk I will survey some lower bounds on other restricted computational models, which include a generalization of our results for backtrack SAT algorithms and proving integrality gaps for Lovasz-Schrijver hierarchy for the linear relaxations of a (hypergraph) vertex cover.

The talk is based on the joint work with: Edward Hirsch, Dmitry Itsykson, Allan Borodin, Joshua Buresh-Oppenheim, Russell Impagliazzo, Avner Magen, Toniann Pitassi Sanjeev Arora, Iannis Tourlakis