Size space tradeoffs for resolution

We investigate tradeoffs of various basic complexity measures such as size, space and width. We show examples of formulas that have optimal proofs with respect to any one of these parameters, but optimizing one parameter must cost an increase in the other. These results have implications to the efficiency (or rather, inefficiency) of some commonly used SAT solving heuristics. Our proof relies on a novel connection of the variable space of a proof to the black-white pebbling measure of an underlying graph.

• Type: Conference
• Year: 2002
• Where: STOC
• Authors: Eli Ben-Sasson
• Keywords: Algorithms, Basic Complexity Measures, Black-white Pebbling Measure, STOC 2002