home · mobile · calendar · colloquia · 1998-1999 · 

Colloquium - Pitassi

Satisfiability and the Efficiency of Resolution
University of Arizona

The importance of the satisfiability problem (SAT) permeates all areas of computer science. In the last three decades, there has been a tremendous amount of research in trying to understand the mathematical structure of the satisfiability problem and in developing good heuristics for SAT and the complementary problem of propositional theorem proving. In fact, there is a resurgence within AI of trying to solve planning and reasoning problems by reductions to (variants of) SAT. The oldest and most well-studied class of algorithms for SAT are resolution-based, with the Davis-Putnam procedure being the most typical example.

We are motivated by trying to uncover a clean combinatorial characterization of the class of formulas exhibiting short resolution refutations. A related goal is to study specific resolution-based algorithms for SAT, and again find a clean characterization of those formulas that are efficiently decided (to be satisfiable or not) by the algorithm. In particular, exactly when will the popular Davis-Putnam procedure find a refutation efficiently? Under which distributions will various heuristics perform well? Is there a "most efficient" resolution-based algorithm for SAT? Obtaining strong lower bounds for resolution necessarily underlies the answers to these questions.

In this talk, we present several new and simple upper and lower bounds for Resolution for specific formulas as well as for randomly generated formulas. Many of our bounds are nearly tight, and our methods reveal that minimum clause size is an important parameter for studying proof length. This idea was used explicitly by Ben-Sassoon and Wigderson very recently to obtain simpler proofs of our results. We will also discuss the related question of whether there is a universal search algorithm for resolution.

This is joint work with Paul Beame, Richard Karp and Mike Saks.

Hosted by Clayton Lewis.

Department of Computer Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
May 5, 2012 (14:13)