Output details

Parameterized Complexity of DPLL Search Procedures

<10>We develop a new game-theoretic proof technique for demonstrating strong lower bounds in tree-like proof systems. This new technique exploits an elegant, intuitive information-theoretic argument. We obtain lower bounds for clique formulas in random graphs in tree-like Resolution. This directly translates into lower bounds for SAT solvers which are widely used in practice. In subsequent work we demonstrate that our method simplifies many previous bounds (http://dx.doi.org/10.1016/j.ipl.2010.09.007) and even guarantees optimal lower bounds (http://dx.doi.org/10.1016/j.ipl.2013.06.002). Our results were included in the textbook "Boolean Function Complexity" (Jukna 2012). Nominated for the best paper award in SAT'11 (three nominations).