Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions

Computer Science – Computational Complexity

Scientific paper

Rate now

  [ 0.00 ] – not rated yet Voters 0   Comments 0

Details

This paper is a merged and updated version of the two ECCC technical reports TR09-034 and TR09-047, and it hence subsumes thes

Scientific paper

For current state-of-the-art DPLL SAT-solvers the two main bottlenecks are the amounts of time and memory used. In proof complexity, these resources correspond to the length and space of resolution proofs. There has been a long line of research investigating these proof complexity measures, but while strong results have been established for length, our understanding of space and how it relates to length has remained quite poor. In particular, the question whether resolution proofs can be optimized for length and space simultaneously, or whether there are trade-offs between these two measures, has remained essentially open. In this paper, we remedy this situation by proving a host of length-space trade-off results for resolution. Our collection of trade-offs cover almost the whole range of values for the space complexity of formulas, and most of the trade-offs are superpolynomial or even exponential and essentially tight. Using similar techniques, we show that these trade-offs in fact extend to the exponentially stronger k-DNF resolution proof systems, which operate with formulas in disjunctive normal form with terms of bounded arity k. We also answer the open question whether the k-DNF resolution systems form a strict hierarchy with respect to space in the affirmative. Our key technical contribution is the following, somewhat surprising, theorem: Any CNF formula F can be transformed by simple variable substitution into a new formula F' such that if F has the right properties, F' can be proven in essentially the same length as F, whereas on the other hand the minimal number of lines one needs to keep in memory simultaneously in any proof of F' is lower-bounded by the minimal number of variables needed simultaneously in any proof of F. Applying this theorem to so-called pebbling formulas defined in terms of pebble games on directed acyclic graphs, we obtain our results.

No associations

LandOfFree

Say what you really think

Search LandOfFree.com for scientists and scientific papers. Rate them and share your experience with other people.

Rating

Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions will most certainly appreciate the feedback.

Rate now

     

Profile ID: LFWR-SCP-O-479231

  Search
All data on this website is collected from public sources. Our data reflects the most accurate information available at the time of publication.