skip to main content
Department of Computer Science University of Colorado Boulder
cu: home | engineering | mycuinfo | about | cu a-z | search cu | contact cu cs: about | calendar | directory | catalog | schedules | mobile | contact cs
home · events · colloquia · 1998-1999 · 

Colloquium - Pitassi

Eaton South

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.

The Department holds colloquia throughout the Fall and Spring semesters. These colloquia, open to the public, are typically held on Thursday afternoons, but sometimes occur at other times as well. If you would like to receive email notification of upcoming colloquia, subscribe to our Colloquia Mailing List. If you would like to schedule a colloquium, see Colloquium Scheduling.

Sign language interpreters are available upon request. Please contact Stephanie Morris at least five days prior to the colloquium.

See also:
Department of Computer Science
College of Engineering and Applied Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
Send email to

Engineering Center Office Tower
ECOT 717
FAX +1-303-492-2844
XHTML 1.0/CSS2 ©2012 Regents of the University of Colorado
Privacy · Legal · Trademarks
May 5, 2012 (13:29)