Jakob Nordström
Short Proofs May Be Spacious: Understanding Space in Resolution
Download
School of Computer Science and Communication, Royal Institute of Technology (KTH) May 2008
Abstract:
Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The two main bottlenecks for such algorithms are the amounts of time and memory used. Thus, understanding time and memory requirements for clause learning algorithms, and how these requirements are related to one another, is a question of considerable practical importance.
In the field of proof complexity, these resources correspond to the length and space of resolution proofs for formulas in conjunctive normal form (CNF). There has been a long line of research investigating these proof complexity measures and relating them to the width of proofs, another measure which has turned out to be intimately connected with both length and space. Formally, the length of a resolution proof is the number of lines, i.e., clauses, the width of a proof is the maximal size of any clause in it, and the space is the maximal number of clauses kept in memory simultaneously if the proof is only allowed to infer new clauses from clauses currently in memory.
While strong results have been established for length and width, our understanding of space has been quite poor. For instance, the space required to prove a formula is known to be at least as large as the needed width, but it has remained open whether space can be separated from width or whether the two measures coincide asymptotically. It has also been unknown whether the fact that a formula is provable in short length implies that it is also provable in small space (which is the case for length versus width), or whether on the contrary these measures are "completely unrelated" in the sense that short proofs can be maximally complex with respect to space.
In this thesis, as an easy first observation we present a simplified proof of the recent length-space trade-off result for resolution in (Hertel and Pitassi 2007) and show how our ideas can be used to prove a couple of other exponential trade-offs in resolution.
Next, we prove that there are families of CNF formulas that can be proven in linear length and constant width but require space growing logarithmically in the formula size, later improving this exponentially to the square root of the size. These results thus separate space and width. Using a related but different approach, we then resolve the question about the relation between space and length by proving an optimal separation between them. More precisely, we show that there are families of CNF formulas of size O(n) that have resolution proofs of length O(n) and width O(1) but for which any proof requires space Omega(n / log n). All of these results are achieved by studying so-called pebbling formulas defined in terms of pebble games over directed acyclic graphs (DAGs) and proving lower bounds on the space requirements for such formulas in terms of the black-white pebbling price of the underlying DAGs.
Finally, we observe that our optimal separation of space and length is in fact a special case of a more general phenomenon. Namely, for any CNF formula F and any Boolean function f : {0,1}^d -> {0,1}, replace every variable x in F by f(x_1, .., x_d) and rewrite this new formula in CNF in the natural way, denoting the resulting formula F[f]. Then if F and f have the right properties, F[f] can be proven in resolution in essentially the same length and width as F but the minimal space needed for F[f] is lower-bounded by the number of variables that have to be mentioned simultaneously in any proof for F.
Table of Contents
Part I: Introduction
1 A Popular Science Introduction
1.1 Let's Get Formal
1.2 Proving Things Is Complex
1.3 What Is a Proof?
1.4 Why Is It Hard to Prove Lower Bounds?
2 Formal Introduction and Results Overview
2.1 Previous Work
2.2 Two Questions Left Open by Previous Research
2.3 Our Contribution
3 High-Level Overview of Tools and Methods
3.1 Sketch of Preliminaries
3.2 Proof Idea for Pebbling Contradictions
3.3 Overview of Formal Proofs of Space Bounds
3.4 Overview of Trade-off Results
3.5 Outline of This Thesis
Part II: Background
4 Proof Complexity and Resolution
4.1 A Proof Complexity Primer
4.2 Definition of the Resolution Proof System
4.3 A Review of Some Results
5 Pebble Games and Pebbling Contradictions
5.1 Pebble Games
5.2 Pebbling Contradictions
6 Pebbling Price of Layered Graphs
6.1 Some Graph Notation and Terminology
6.2 Pebbling Price of Binary Trees
6.3 The Black Pebbling Price of Pyramids
6.4 Black-White Pebbling Pyramids---a First Bound
6.5 A Tight Bound for Black-White Pebbling
Part III: On Space in Resolution
7 A Simplified Way of Proving Trade-offs
7.1 A Proof of Hertel and Pitassi's Trade-off Result
7.2 Some Other Trade-off Results for Resolution
7.3 Making the Main Trick Explicit
7.4 An Auxiliary Trick for Variable Space
8 A Separation of Space and Width
8.1 Overview of Space-Width Separation Proof
8.2 The Labelled Pebble Game
8.3 Resolution Derivations Induce Labelled Pebblings
8.4 Induced L-pebbles Measure Clause Set Size
8.5 The Labelled Pebbling Price of Binary Trees
9 Towards Separating Space and Length
9.1 Overview of Improved Lower Bound Proof
9.2 The Blob-Pebble Game
9.3 Resolution Derivations Induce Blob-Pebbling
9.4 Induced Blob Configurations and Clause Set Size
9.5 A Tight Bound for Blob-Pebbling the Pyramid
10 Short Proofs May Be Spacious
10.1 Outline of Proof of a Special Case
10.2 Generalized Pebbling Contradictions
10.3 The Resolution-Pebbling Game
10.4 Derivations Induce Resolution-Pebblings
10.5 Res-Pebbling Price Lower-Bounds Space
11 Understanding Space in Resolution
11.1 Substitution Formulas and Variable Support Size
11.2 A General Theorem on Substitution and Space
11.3 Proof Sketch for the Substitution Space Theorem
Part IV: Conclusion
12 Concluding Remarks
12.1 Resolution Refutation Space of Pebbling Contradictions
12.2 Space Lower Bounds for Stronger Proof Systems
12.3 Trade-off Questions for Resolution
