Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 0803.0661

Towards an Optimal Separation of Space and Length in Resolution

Jakob Nordström·Johan Håstad
View original source ↗Read source document ↗Export metadata ↓

Abstract

Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The main bottleneck for such algorithms, other than the obvious one of time, is the amount of memory used. In the field of proof complexity, the resources of time and memory correspond to the length and space of resolution proofs. There has been a long line of research trying to understand these proof complexity measures, but while strong results have been proven on length our understanding of space is still quite poor. For instance, it remains open whether the fact that a formula is provable in short length implies that it is also provable in small space or whether on the contrary these measures are unrelated in the sense that short proofs can be arbitrarily complex with respect to space. In this paper, we present some evidence that the true answer should be that the latter case holds. We do this by proving a tight bound of Theta(sqrt(n)) on the space needed for so-called pebbling contradictions over pyramid graphs of size n. This yields the first polynomial lower bound on space that is not a consequence of a corresponding lower bound on width, another well-studied measure in resolution, as well as an improvement of the weak separation in (Nordstrom 2006) of space and width from logarithmic to polynomial. Also, continuing the line of research initiated by (Ben-Sasson 2002) into trade-offs between different proof complexity measures, we present a simplified proof of the recent length-space trade-off result in (Hertel and Pitassi 2007), and show how our ideas can be used to prove a couple of other exponential trade-offs in resolution.

Explore related subjects

cs.CCcs.LO

Keep this discovery

BibTeXRIS

Jakob Nordström, Johan Håstad. 2008-03-05. Towards an Optimal Separation of Space and Length in Resolution. https://arxiv.org/abs/0803.0661

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

The Computational Complexity of Holant Problems on 4-regular Graphs from the Stable Subgroup Sequence of $SL(2,\mathbb{C})$

The Holant framework provides a general setting for studying counting problems and includes graph homomorphisms (\#GH) and counting constraint satisfaction problems (\#CSP) as special cases. Over the past twenty years, a series of computational complexity dichotomies have been established for Holant problems, but the classification for complex-valued signatures is still open. The main obstacle is the case in which all signatures have even arity. In this paper, we establish a dichotomy for Holant problems with a complex-valued 4-ary signature, which is a key base case for the full classification of Holant problems. We present a new strategy by introducing Schur's theorem, the classification of finite subgroups of $\mathrm{SL}(2,\mathbb{C})$ and stable subgroup sequences into the proof. These new techniques are of independent interest.

cs.CC↗
arXiv2026

Topology inside NC$^1$

We show that ACC$^0$ is precisely what can be computed with constant-width circuits of polynomial size and polylogarithmic genus. This extends a characterization given by Hansen, showing that planar constant-width circuits also characterize ACC$^0$. Thus polylogarithmic genus provides no additional computational power in this model. We consider other generalizations of planarity, including crossing number and thickness. We show that constant-width circuits of polynomial size and thickness two already suffice to capture all of NC$^1$.

cs.CC↗