TR22-054 Authors: Anastasia Sofronova, Dmitry Sokolov

Publication: 24th April 2022 22:14

Downloads: 537

Keywords:

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).