arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 0707.4255

Complexity of Propositional Proofs under a Promise

Nachum Dershowitz·Iddo Tzameret
View original source ↗Read source document ↗Export metadata ↓

Abstract

We study -- within the framework of propositional proof complexity -- the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiable formula has many satisfying assignments, where ``many'' stands for an explicitly specified function $\Lam$ in the number of variables $n$. To this end, we develop propositional proof systems under different measures of promises (that is, different $\Lam$) as extensions of resolution. This is done by augmenting resolution with axioms that, roughly, can eliminate sets of truth assignments defined by Boolean circuits. We then investigate the complexity of such systems, obtaining an exponential separation in the average-case between resolution under different size promises: 1. Resolution has polynomial-size refutations for all unsatisfiable 3CNF formulas when the promise is $\eps\cd2^n$, for any constant $0<\eps<1$. 2. There are no sub-exponential size resolution refutations for random 3CNF formulas, when the promise is $2^{δn}$ (and the number of clauses is $o(n^{3/2})$), for any constant $0<δ<1$.

Explore related subjects

cs.CCcs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Nachum Dershowitz, Iddo Tzameret. 2007-07-28. Complexity of Propositional Proofs under a Promise. https://arxiv.org/abs/0707.4255

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

KEEP EXPLORING

Related papers

arXiv2026

Unconditional Separation between LL and CLL

Catalytic computation involves the study of Turing machines that are provided an additional catalytic tape (with arbitrary content) that the machine may use while ensuring that the tape contents are restored at the end of the computation. Although it is known that catalytic log-space machines are at least as powerful as non-deterministic log-space (and more), we do not have unconditional asymptotic separations. In this work, we prove an unconditional separation between a deterministic space complexity class and its catalytic counterpart. More precisely, at the doubly logarithmic scale, we show that catalytic Turing machines can provably compute more languages than standard deterministic doubly-logarithmic space machines. The separation is witnessed by the unary language $\mathrm{POW2} = \{1^n : n \text{ is a power of two}\}$. We construct a catalytic Turing machine that uses $O(\log \log n)$ bits of space and $O(\log n)$ bits of catalytic tape to decide $\mathrm{POW2}$, whereas any standard deterministic Turing machine requires $Ω(\log n)$ space to decide it.

cs.CC↗
arXiv2026

Exponentially Fewer-Server PIR from Sparser $S$-Decoding Polynomials

We show that under a plausible number-theoretic conjecture, for any constant $s$ there exists an $s$-server private information retrieval (PIR) protocol that on an $n$-bit database requires communication $\exp(O((\log n)^{1/s} (\log \log n)^{1-1/s}))$. This achieves a superpolynomial improvement in communication when $s \geq 4$; previous constructions attaining the same communication required $2^{O(s)}$ servers. Our number-theoretic conjecture is implied by existing conjectures, namely the generalized repunit conjecture and Schinzel's hypothesis H (either one of these conjectures would suffice alone). Our result builds on the "matching vector family + $S$-decoding polynomials" framework pioneered by Efremenko (STOC 2009) and recently refined by Ghasemi, Kopparty, and Sudan (STOC 2025). The main ingredient is a framework for constructing $S$-decoding polynomials with only $k+1$ nonzero coefficients modulo special products of $k$ primes, resolving an open problem posed by Ghasemi and Kopparty (ITCS 2026). By the lower bound shown by Ghasemi and Kopparty, this is the minimum achievable sparsity. We also empirically validate our construction and make our result unconditional for all $s \leq 15$. We also apply our techniques to regimes where $s$ grows with $n$, showing under a stronger variant of our number-theoretic conjecture that the communication complexity of $s$-server matching-vector PIR can be superpolynomially reduced from the previous state of the art for any $s \leq \exp(o(\sqrt{\log \log n/\log \log \log n}))$. The main result for $s = O(1)$ and its proof were discovered in a GPT-5.5 Pro conversation prompted by the authors.

cs.CC↗
arXiv2026

Metric Dimension is NP-complete on Graphs of Treewidth Two

The metric dimension of a connected graph is the least number of vertices whose distance vectors distinguish all vertices. We show that deciding whether the metric dimension of a graph is at most a given integer is NP-complete on graphs of treewidth at most two. As the problem is polynomial on trees, the graphs of treewidth one, this settles the treewidth threshold of its hardness, which was known to lie between two and twenty-four. The reduction is from satisfiability of formulas in which every literal occurs at most twice. To such a formula with $n$ clauses and $r$ variables it associates a graph $G_φ$ of treewidth at most two with $O((n+r)^2)$ vertices, whose metric dimension is $2(n+r)+5$ if the formula is satisfiable and $2(n+r)+6$ otherwise.

cs.CC↗