On the Automatability of Tree-Like $k$-DNF Resolution

We prove our result under the randomized exponential time hypothesis which we introduce next. The exponential time hypothesis (ETH), is the strengthening of the $\text{P}\ne \text{NP}$ conjecture, introduced by Impagliazzo and Paturi [24], that states that 3-$\mathrm{𝖲𝖠𝖳}$ cannot be solved in subexponential time. More formally, it states that there exists an $\epsilon >0$ such that 3-$\mathrm{𝖲𝖠𝖳}$ for $n$-variate formulas cannot be decided in deterministic time $2^{\epsilon n}$. The randomized exponential time hypothesis (rETH), introduced by Dell et al. [19], is instead a strengthening of the $\text{NP}⊈\mathrm{𝖡𝖯𝖯}$ conjecture. It asserts that there exists $\epsilon >0$ and $c>1$ such that 3-$\mathrm{𝖲𝖠𝖳}$ for $n$-variate formulas with $cn$ clauses cannot be decided in randomized time $2^{\epsilon n}$.

Our main result is that for any function $k=k(n)\le \log n$, if tree-like Res($k$) is automatable in time $N^{o\left(\frac{k}{\log k}\cdot \log N\right)}$, then rETH is false. We defer the definition of the Res($k$) proof system to Section 2, but note here that in this work – and also in many others – the argument $n$ of the function $k(n)$ is the number of variables in the formula (and does not depend on the size of the proof as per Krajicek’s original definition [27]).

This implies that, under rETH, the algorithm of [4] that automates tree-like Res($k$) in time $N^{O\left(k\cdot \log N\right)}$ is tight up to a $\log k$ factor in the exponent. Previously, the best known lower bound under rETH, for both tree-like resolution and tree-like Res($k$), was $N^{\mathrm{\Omega }\left(\log N\right)}$ [16].

Theorem 1 is a consequence of the following result, which is our main technical contribution.

The proof that Theorem 1 follows from Theorem 2 is quite standard. We refer the reader to the full version of this paper for details. We now focus on the strategy and the new ideas required to prove Theorem 2.

The overall structure of the proof of Theorem 2 follows the general strategy of Atserias and Müller [6], and uses ideas from [18] and [16]. In what follows, we briefly summarize these results, and after that we discuss the challenges encountered to prove our main theorem, and the new ideas needed to overcome them.

The main technical theorem in [6], which yields the NP-hardness of automating resolution, is given below.

The starting point of the algorithm $𝒜$ is to build the formula $\mathrm{Ref}(F,s)$ that encodes, in a natural way, that $F$ has a (DAG-like) resolution refutation of size at most $s$. The idea for building this formula to obtain a large gap between the size of refutation depending on whether $F$ is satisfiable or not comes from Pudlák [34], inspired by Razborov [36]. Pudlák [34] showed that if $F$ is satisfiable then $\mathrm{Ref}(F,s)$ has a short resolution refutation. Intuitively, this refutation uses a satisfying assignment $x^{\ast }$ for $F$ as a guide to find an incorrect step in the purported refutation of $F$, which must exist since $x^{\ast }$ satisfies all clause in $F$ but falsifies the final empty clause.

Proving a lower bound for $\mathrm{Ref}(F,s)$ when $F$ is unsatisfiable turns out to be more challenging and, to address this, Atserias and Müller [6] define a relativized or lifted version of $\mathrm{Ref}(F,s)$ for which they can prove the lower bound and, at the same time, show that the upper bound still holds. In [18] a similar formula is defined and the result is extended to the algebraic proof systems polynomial calculus and Nullstellensatz. The main novelty of [18] is to show that the lower bound can be proven by a reduction from the pigeonhole principle. Finally, in [16], it is shown that, unless rETH is false it is not possible to automate tree-like resolution in time $n^{o(\log n)}$. The main idea of this result is to define a blown-up version of $\mathrm{Ref}(F,s)$ of size $\exp (\mathrm{\Theta }(\sqrt{n}))$ such that, when $F$ is satisfiable, there is a tree-like Resolution refutation of this formula in size $\exp (\mathrm{\Theta }(\sqrt{n}))$.

In most of the follow-up works to [6], the main technical challenge was to show that, when $F$ is unsatisfiable, there exist no small refutations of $𝒜(F)$ for some proof system $𝒫$, which was typically stronger than resolution. For tree-like resolution, however, the main difficulty is quite different. Pudlák’s upper bound [34] for the case where $F$ satisfiable is inherently DAG-like, and the best known tree-like resolution refutations are of exponential size. In fact, we do not expect significantly smaller tree-like resolution refutations of $\mathrm{Ref}(F,s)$ to exist. In particular, if there were such refutations of polynomial size, then the algorithm of [7] that automates tree-like resolution in quasi-polynomial time would imply that NP is in quasi-polynomial time. Overcoming this limitation requires a substantial modification to the structure of $𝒜(F)$.

The key insight of [16] is that one can (randomly) construct a much larger formula, denoted $\mathrm{ShallowRef}(F)$, of size $\exp (\mathrm{\Theta }(\sqrt{n}))$, such that, when $F$ is satisfiable, $\mathrm{ShallowRef}(F)$ admits a tree-like resolution refutation also of the size $\exp (\mathrm{\Theta }(\sqrt{n}))$.¹¹1In [16], it is mistakenly stated that this can be achieved without randomness. However, the construction of $\mathrm{ShallowRef}(F)$ in [16] relies on polynomially unbalanced expander graphs with constant degree, and these are only known to constructable in randomized polynomial time. Together with an exponential lower bound in the casa $F$ is unsatisfiable, this construction yields that automating tree-like resolution in time $n^{o(\log n)}$ would lead to a randomized algorithm for SAT running in time $\exp (o(n))$.

This non-automatability result also extends to tree-like Res($k$). However, for this system, the best known automating algorithm – due to Atserias and Bonet [4] – runs in time $n^{c\cdot k\log n}$. To show that this upper bound is (nearly) tight, we must construct a smaller formula which also admits a smaller tree-like Res($k$) refutation when $F$ is satisfiable. In order to understand the challenge we face in obtaining a better non-automatability result for tree-like Res($k$), we need to describe in more detail the formula $\mathrm{ShallowRef}(F)$, which we do in Section 2. For now, we note that [16] actually shows that we can construct formulas $𝒜(F)$ with the following trade-off: for any size parameter $\log n\le s\le n$, it is possible to construct a formula ${𝒜}_s(F)$ of size $2^{O(s)}$ such that the upper bound for refuting ${𝒜}_s(F)$ when $F$ is satisfiable is $2^{O(n/s)}$. In order to obtain our non-automatability result for tree-like Res($k$), however, we would need that both the formula $𝒜(F)$ and the upper bound be of size roughly $2^{O(\sqrt{n/k})}$.

We present the intuition behind the construction of $𝒜(F)$ in the next section. One of the core technical challenges is efficiently representing and accessing objects of size $2^{\sqrt{nk}}$ within a formula whose size is only $2^{\sqrt{n/k}}$. We would like to represent such objects via pigeonhole principle instances, but the naive encoding would produce a formula of size $2^{\sqrt{nk}}$. The key insight is to instead use small circuits that compute the neighbor function of an unbalanced expander graph used for defining the pigeonhole principle instances. These circuits act as shortcuts for accessing the larger set of objects, allowing us to simulate the effect of having access to $2^{\sqrt{nk}}$ items within a formula of size $2^{\sqrt{n/k}}$.

For the lower bound, our argument builds on the strategy in [18], which relies on a low-depth reduction from the pigeonhole principle. However, in our case, the formula incorporates different types of unbalanced expanders, making it difficult to reduce from a single pigeonhole principle instance, as was done previously. To address this, we introduce a generalized reduction that maps multiple formulas to a single formula. We note that even in [18], using these generalized reductions would have slightly improved the parameters, making them match those of [6].

We are now ready to state Theorem 1 formally.

The proof of this theorem follows from Theorem 2 in a rather straightforward way. The only aspect that needs some care is to choose the $k$ that should be given as input to the randomized algorithm $𝒜$ of Theorem 2. We leave the details of this proof to the full-length version of this paper.

Before we present the intuition behind the construction of the formula $𝒜(F)$, we introduce some graph theory notation and define the expander graphs that we use to construct the formula $𝒜(F)$. We refer the reader to, e.g., [10] for missing basic definitions in graph theory.

In this paper, graphs $G=(V,E)$ are simple and undirected. We often identify the vertex set $V$ of a graph with the subset $[|V|]$ of $\mathbb{N}$, and assume that the vertices of the graph inherit the standard ordering of $\mathbb{N}$. A $d$-regular graph is a graph where every vertex has degree exactly $d$. In the context of bipartite graphs, we say that $\mathrm{\Gamma }=(L\dot{\cup }R,E)$ is left $d$-regular graph (resp., right $d$-regular graph) if and only if all its vertices in $L$ (resp., $R$) have degree $d$. Given a graph $G=(V,E)$, and a subset of the its vertex set $S\subseteq V$, we define the neighborhood of $S$, denoted as $𝒩(S)$, to be the set of all vertices in $V$ which are adjacent to some vertex in $S$. Formally, $𝒩(S)=\{v\in V:\exists u\in S,\{u,v\}\in E\}$. We assume that the neighbors of a vertex are ordered according to an arbitrary yet fixed ordering. We define the following function that allows us to access the neighbors of a vertex.

We now define the types of expander graphs which appear in this work.

We are interested in unbalanced bipartite expander graphs with small left degree. For our purposes, we require more than the existence of such expander graphs – we need there to be a small circuit that computes its neighbor function and, moreover, these circuit must be constructable in randomized polynomial time.

The proof of this theorem uses known constructions of $k$-independent functions, and can be found in the full-length version of this paper. We are now ready to describe the main ideas needed for the construction $𝒜(F)$.

Let $F$ be a CNF formula over variables $x_1,\mathrm{\dots },x_n$ with $\mathrm{𝗉𝗈𝗅𝗒}(n)$ clauses. The $\mathrm{Ref}(F,s)$ formula encodes that there is a resolution refutation of $F$ of size $s$, which is usually chosen to be a polynomial in $n$. As mentioned earlier, Pudlák’s [34] upper bound for $\mathrm{Ref}(F,s)$ when $F$ is satisfiable, which was adapted in [6], is intrinsically DAG-like. We do not expect there to be polynomial-size tree-like $\mathrm{Res}(k)$ refutations of $\mathrm{Ref}(F,s)$ for satisfiable $F$ since, due to the quasi-polynomial algorithm that automates tree-like $\mathrm{Res}(k)$, this would imply that it is possible to solve SAT in quasi-polynomial time. It may be the case that tree-like $\mathrm{Res}(k)$ requires size at least $2^{\mathrm{\Omega }(n)}$ to refute $\mathrm{Ref}(F,s)$, regardless of whether $F$ is satisfiable and, therefore, it seems that non-automatability results for tree-like $\mathrm{Res}(k)$ are unlikely to be obtained using this formula.

In order to describe the formula ${\mathrm{ShortcutRef}}_k(F)$ we first describe a simplified version of ${\mathrm{ShortcutRef}}_1(F)$, which is inspired by the formula $\mathrm{ShallowRef}(F)$ from [16]. Consider the trivial tree-like resolution refutation of a formula $F$, denoted by $\mathrm{\Pi }$, corresponding to the refutation of depth $n$ that has $2^n$ leaves, one for every width-$n$ clause (each of which is a weakening of some axiom), and that resolves over variables in reverse order, that is, $x_n$ then $x_{n-1}$, etc., until it resolves over $x_1$ to derive the empty clause. We view the clauses of this refutation as arranged in layers, and we say that all clauses that are obtained by resolving over variable $i$ are in layer $i$.

We can create a formula stating that this tree-like resolution refutation fits into a smaller structure as follows (see Figure 1). The variables of this formula are partitioned into blocks, one block for each clause of the purported structured derivation. The structure of the blocks is as follows. We start from the top of the refutation (the part closest to $\perp$) and for the first $2q$ layers we simply copy the first $2q$ layers of $\mathrm{\Pi }$ (i.e., copy the structure and the clauses). At this point, we have $2^{2q}$ leaves and our structure is starting to get too big. We therefore create a new layer with only $2^q$ blocks and encode (the contradictory statement) that, actually, the $2^{2q}$ blocks of the layer above can be mapped in a one-to-one fashion to these $2^q$ new blocks. This mapping is encoded by enforcing that if block $B$ is mapped to block $B^{\prime }$ then both contain the exact same clause. Starting from each of the $2^q$ new blocks, we construct a full binary tree of blocks of depth $q$. This gives us $2^{2q}$ blocks at the last layer and we again map these blocks to $2^q$ blocks. By repeating this procedure $n/q$ times, we create a structure of depth $n$, but that has size only $2^{O(q)}$. For reasons that will become clear soon, we encode the mapping from $2^{2q}$ to $2^q$ as a pigeonhole principle instance over an expander of constant degree $\mathrm{\Delta }$. Note that this structure has size $2^{O(q)}$.

We can define a formula, which we refer to ${\mathrm{ShortcutRef}}_1^{\star }(F)$ (see Figure 1), of size $2^{O(q)}$ that encodes that a resolution refutation with this structure exists. For some intuition as to why ${\mathrm{ShortcutRef}}_1^{\star }(F)$ could give us a non-automatability result for tree-like resolution, observe that, if $F$ is unsatisfiable, the only reason ${\mathrm{ShortcutRef}}_1^{\star }(F)$ is unsatisfiable is that we cannot have a one-to-one map from $2^{2q}$ blocks to $2^q$ blocks. Since pigeonhole principle formulas over expander graphs are hard to refute for resolution, it is reasonable that ${\mathrm{ShortcutRef}}_1^{\star }(F)$ should be hard to refute for resolution (and thus also for tree-like resolution).

When $F$ is satisfiable, however, there is another reason ${\mathrm{ShortcutRef}}_1^{\star }(F)$ is unsatisfiable: there is an assignment $x^{\ast }$ that satisfies all clauses in $F$. A proof that ${\mathrm{ShortcutRef}}_1^{\star }(F)$ is unsatisfiable corresponds to showing that, no matter what purported refutation of $F$ is (that fits in the structure), it will contain a mistake. It is too early to get into many details here, but the rough intuition is that a tree-like resolution refutation of ${\mathrm{ShortcutRef}}_1^{\star }(F)$ can be viewed as following a path from the clause $\perp$ to a clause at the bottom of the structure of ${\mathrm{ShortcutRef}}_1^{\star }(F)$ keeping the invariant that $x^{\ast }$ falsifies all clauses of the purported refutation ${\mathrm{ShortcutRef}}_1^{\star }(F)$ it goes through. If we did not find a mistake in the purported refutation earlier, once we reach a clause $C$ at the bottom layer we necessarily find a mistake, since by the invariant $x^{\ast }$ falsifies $C$, but it satisfies all clauses of $F$, so $C$ cannot be a weakening of an axiom of $F$.

This argument can be carried out in tree-like resolution in size which is proportional to the number of paths from the top block to a block at the bottom layer in ${\mathrm{ShortcutRef}}_1^{\star }(F)$. If we did not have an expander graph between layers, but instead had a complete bipartite graph, the number of such paths would be ${(2^q)}^{n/q}=2^n$, which is too large. With bipartite expander graphs with maximum left-degree $\mathrm{\Delta }$, the number of such paths becomes ${\mathrm{\Delta }}^{n/q}$. If we define $q=\sqrt{n}$, we have that the size of the formula ${\mathrm{ShortcutRef}}_1^{\star }(F)$ and the upper bound when $F$ is satisfiable is $2^{O(\sqrt{n})}$. This, together with a size lower bound of $2^{\mathrm{\Omega }(n)}$ for refuting ${\mathrm{ShortcutRef}}_1^{\star }(F)$ when $F$ is unsatisfiable, gives the non-automatability result for tree-like resolution in [16].

This result for tree-like resolution also applies for tree-like $\mathrm{Res}(k)$, but our goal is to prove a stronger non-automatability result for tree-like $\mathrm{Res}(k)$. To this end, we want to design a formula that is both smaller and for which we get a smaller tree-like $\mathrm{Res}(k)$ refutation when $F$ is satisfiable. The best one could hope for, without contradicting ETH, is that both the size and the upper bound become $2^{O(\sqrt{n/k})}$. By varying $q$, we can make either of the parameters small, but not both at the same time. In particular, if we consider ${\mathrm{ShortcutRef}}_1^{\star }(F)$ with $q=\sqrt{nk}$ we get an upper bound of $2^{O(\sqrt{n/k})}$, at the cost of increasing the size of the formula to $2^{\mathrm{\Theta }(\sqrt{nk})}$. (Note that the upper bound is smaller than the size of the formula since by definition of refutation size we only count the clauses used in the refutation.) In particular, between two “shrinking layers”, we have trees of size $2^{\sqrt{nk}}$.

Here is where our modules comes into play. Let $C$ be the root of one of the trees of size $2^{\sqrt{nk}}$. Instead of encoding that there is a tree-like derivation of $C$ from the $2^{\sqrt{nk}}$ leaves, we encode that there is size-$s$ resolution derivation of $C$ from only $m=2^{\sqrt{n/k}}$ clauses. This can be done using a formula that is structurally close to $\mathrm{Ref}(F,s)$, except that instead of a fixed $F$ we have blocks encoding potential axioms $A_1,\mathrm{\dots },A_m$, and we do not enforce that the last block is the empty clause. We denote the formula encoding this small derivation by ${\mathrm{Mod}}_{s,m}$.

We can use these formulas ${\mathrm{Mod}}_{s,m}$ to obtain a formula similar to ${\mathrm{ShortcutRef}}_1^{\star }(F)$ but of size $2^{O(\sqrt{n/k})}$ as follows. Observe that after each layer of $2^{\sqrt{n/k}}$ modules we have $2^{\sqrt{n/k}}$ sets of $m=2^{\sqrt{n/k}}$ axioms $A_1,\mathrm{\dots },A_m$. We now define the graph PHP formula over blocks that map these ${(2^{\sqrt{n/k}})}^2$ blocks to $2^{\sqrt{n/k}}$ blocks. To build this formula we use a bipartite expander graphs, shrinking expanders, that plays the analogous role as the expander graph in ${\mathrm{ShortcutRef}}_1^{\star }(F)$.

While the formula obtained at this point has the correct size, we need to ensure that the upper bound can go through. To this end, we need to be able to easily access any of the $2^{\sqrt{nk}}$ extensions of $C$. We therefore encode an additional graph PHP formula over an expander graph, the shortcut expander, that maps $2^{\sqrt{nk}}$ partial assignments to the $2^{\sqrt{n/k}}$ blocks corresponding to $A_1,\mathrm{\dots },A_m$. This expander graph is too large to be hardcoded (the whole point is that we are trying to get the formula size down to $2^{\sqrt{n/k}}$) so we instead encode a circuit of size $2^{O(\sqrt{n/k})}$ that computes the neighbor function of this graph. With some other minor technicalities, like adding some extension variables, we can obtain an upper bound of roughly $k^{O(\sqrt{n/k})}$. This would already give us a good non-automatability result, but we can get a bit better by balancing the size of the formula and the upper bound. This is why the precise parameters of our formula ${\mathrm{ShortcutRef}}_k(F)$ presented in the next section differ slightly from the ones presented here.

We start by defining the formula ${\mathrm{Mod}}_{s,m}$ which we refer to as a module. This formula is similar to ${\mathrm{Ref}}_s(F)$, except that instead of a fixed $F$ we have $m$ blocks encoding potential axioms, and we do not enforce that the last block is the empty clause.

We now define the graph-PHP formula over blocks that will be necessary to reduce the size of the final formula. Given $M,N,\mathrm{\Delta }\in \mathbb{N}$, with $\mathrm{\Delta }\le N\le M$, and given a bipartite graph $\mathrm{\Gamma }=(([M],[N]),E)$ with uniform left degree $\mathrm{\Delta }$, we define the formula $\mathrm{ShrinkBlocks}(\mathrm{\Gamma })$ which encodes the statement, which is contradictory when $M>N$, that there is a subset of edges of $E$ that define an injective map from $M$ blocks to $N$ blocks. We assume for simplicity that $N$ is a power of $2$.

Let $M,N,\mathrm{\Delta }\in \mathbb{N}$, with $\mathrm{\Delta }\le N\le M$, and assume for simplicity that $M$ and $N$ are a power of $2$. Given a circuit $𝒞$ of size $S$ encoding the neighbor function of a bipartite graph $\mathrm{\Gamma }=(([M],[N]),E)$ with uniform left degree $\mathrm{\Delta }$, we define the auxiliary formula $\mathrm{ShortcutBlocks}(𝒞,t)$ which encodes the statement, which is contradictory when $M>N$, that there is an injective map from $M$ blocks to $N$ blocks.

We start by considering $\mathrm{\Delta }$ circuits ${𝒞}_j$ for $j\in [\mathrm{\Delta }]$, where the ${𝒞}_j$ is obtained by fixing the second part of the input of $𝒞$ to be $j$. Note that such a ${𝒞}_j$ computes the $j$th neighbor of the input vertex. We first define a formula that encodes the circuit ${𝒞}_j$.

Given a CNF formula $F$ over variables $x_1,\mathrm{\dots },x_n$ with $m=\mathrm{𝗉𝗈𝗅𝗒}(n)$ clauses, and an integer $k\in [n]$, we can now explain how to put these building blocks together to construct ${\mathrm{ShortcutRef}}_k(F)$.

Let $r=\sqrt{n/k\log k}$, $q=\sqrt{(n\log k)/k}$, $c=2^q$ and $s=nc$. We consider $rc$ copies of the module ${\mathrm{Mod}}_{s,c}$ arranged in $r$ layers, $c$ copies per layer. For every block $B$ appearing in ${\mathrm{Mod}}_{s,c}$, we denote by $B[i,j]$ the $j$th copy of the block in layer $i$.

The proof follows the general strategy of the upper bound proof for $\mathrm{Ref}(F)$ as presented in, e.g., [18]. Recall that the ${\mathrm{ShortcutRef}}_k(F)$ formula is organized as a grid of modules with $r=$ layers and $c=$ modules per layer, and ${\mathrm{\Delta }}_{\mathrm{sc}}=O(k)$ is the degree of the expander graph encoded in the subformulas $\mathrm{ShrinkBlocks}({\mathrm{\Gamma }}_{\mathrm{sh}})$ of $\mathrm{ShortcutRef}$.

Given a block $B$ of ${\mathrm{ShortcutRef}}_k(F)$, we refer to the clause encoded by the variables ${\text{lit}}_{\mathrm{\ell }}^B$ to be the clause at block $B$.

We start by explaining how to define a decision tree (that is, a $1$-decision tree) that solves $\mathrm{𝖲𝖾𝖺𝗋𝖼𝗁}({\mathrm{ShortcutRef}}_k(F))$ when $F$ is satisfiable. The only problem with this upper bound is that it will be too large. We later explain how $k$-decision trees can use the shortcuts of ${\mathrm{ShortcutRef}}_k(F)$ to yield a better upper bound.

Let $x^{\ast }$ be a satisfying assignment of $F$. Starting at root block $D_{s+1}[1,1]$, we can query the enabled variable and, one by one, all literal variables that $x^{\ast }$ satisfies. Either we have found a falsified clause (one of the root axioms) or we have that the root block is enabled and has a clause with no literals, which therefore is falsified by $x^{\ast }$. The goal is to move down the blocks of ${\mathrm{ShortcutRef}}_k(F)$ until we reach the axiom blocks at the last layer, all the while keeping the invariant that the block we are at is enabled and contains a clause that is falsified by $x^{\ast }$. In this process, we either find a non-sound step, which immediately gives us a falsified clause of ${\mathrm{ShortcutRef}}_k(F)$, or the path reaches an axiom block at the last layer. If we reach an axiom block $A$ at the last layer while keeping the invariant, we can easily find a falsified clause of ${\mathrm{ShortcutRef}}_k(F)$. Indeed, since $x^{\ast }$ falsifies the clause at block $A$ but $x^{\ast }$ satisfies all clauses of $F$, one of the axioms of ${\mathrm{ShortcutRef}}_k(F)$ encoding that the clause at $A$ must be a weakening of some clause in $F$ will be falsified.