Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR22-054 | 21st April 2022 16:05

A Lower Bound for $k$-DNF Resolution on Random CNF Formulas via Expansion


Authors: Anastasia Sofronova, Dmitry Sokolov
Publication: 24th April 2022 22:14
Downloads: 701


Random $\Delta$-CNF formulas are one of the few candidates that are expected to be hard to refute in any proof system. One of the frontiers in the direction of proving lower bounds on these formulas is the $k$-DNF Resolution proof system (aka $\mathrm{Res}(k)$). Assume we sample $m$ clauses over $n$ variables. There are two known lower bounds.
1. Segerlind, Buss, Impagliazzo showed an exponential lower bound for any constant $k$, $\Delta = \mathcal{O}(k^2)$ in case $m = \mathcal{O}(n^{7 / 6})$.
2. Alekhnovich showed lower bound for $k = \mathcal{O}(\sqrt{\frac{\log n}{\log\log n}})$, any $\Delta \ge 3$ in case $m = \mathcal{O}(n)$.

Both of these papers used the same technique: the so-called small restriction switching lemma. However, they used different properties of the dependency graph of the random formula. In this paper we present a new technique with the same flavour though based on a different complexity measure that we call closure covering. We use only the expansion of the dependency graph of the formula. This technique allows us to unify and improve both of these bounds simultaneously. In particular, as a corollary we show:
1) an exponential lower bound for any constant $k$, $\Delta = \mathcal{O}(1)$ in case $m = \mathrm{poly}(n)$;
2) an exponential lower bound for $k = \mathcal{O}(\sqrt{\log n})$, $\Delta = \mathcal{O}(1)$ in case $m = \mathcal{O}(n)$.

It is the first lower bound that works for clause density $\frac{m}{n} > n^{1 / 6}$ (density can even be superpolynomial for random $\log n$-CNF).

ISSN 1433-8092 | Imprint