1 Introduction↩︎

1.0.0.1 Meta-Complexity

One of the main goals of the area of meta-complexity is to prove strong hardness results for computing complexity measures such as circuit size, formula size and monotone circuit size. While such hardness results can be derived in a standard way from cryptographic assumptions such as the existence of one-way functions [2], [3], it has proven much more challenging to show hardness results under worst-case assumptions, such as \(\mathsf{NP}\)-hardness results. A good reason for this difficulty was identified by Kabanets and Cai [3], who showed that \(\mathsf{NP}\)-hardness of the Minimum Circuit Size Problem (which asks whether a Boolean function F given by its truth table has circuits of size at most \(s\), for a given parameter \(s\)) via polynomial-time honest reductions would imply hard-to-prove circuit lower bounds such as super-polynomial circuit lower bounds for \(\mathsf{EXP}\).

Despite this obstacle, there are now several hardness results for various notions of circuit size under worst-case hardness assumptions, including DNF size, Boolean formula size (under ETH), multi-output circuit size, oracle circuit size, etc., [4]–[12]. A common feature of these results, except for the recent inapproximability result of [12] for oracle circuit size, is that they do not show strong inapproximability results for circuit size. Here, by a strong inapproximability result, we mean the hardness of approximating the circuit size within a \(N^{\Omega(1)}\) multiplicative factor, where \(N\) is the size of the function representation.

A major motivation for showing strong inapproximability result for circuit size under worst-case assumptions is that they offer a pathway to worst-case to average-case reductions for \(\mathsf{NP}\). It was shown in [13], [14], building on work of [15], that there are non-black-box reductions from strong inapproximability of problems such as circuit size and average circuit size to average-case hardness for these problems. Thus, \(\mathsf{NP}\)-hardness of strong inapproximability for either of these problems would rule out Heuristica, the complexity world imagined by Impagliazzo [16] where \(\mathsf{NP}\) is hard in the worst case but easy on average. A recent result of Mazor and Pass [17] rules out strong inapproximability of circuit size under Levin reductions from SAT, assuming a standard cryptographic assumption, but strong inapproximability might still hold under a more general notion of reduction such as Turing reductions. The strong inapproximability result of [12] for oracle circuit size is based on cryptographic techniques and seems difficult to apply to standard circuit size measures. It could potentially be very useful to find other techniques yielding strong inapproximability.

In terms of circuit size measures for which hardness under worst-case assumptions is known, monotone circuit size has been little-studied despite its central role in complexity theory. Showing \(\mathsf{NP}\)-hardness for the Minimum Monotone Circuit Size Problem (which asks whether a monotone Boolean function given by its truth table has monotone circuit size at most \(s\), for a given parameter \(s\)) would be a significant step towards \(\mathsf{NP}\)-hardness for the Minimum Circuit Size Problem, as there is a well-known reduction from Minimum Circuit Size to Minimum Monotone Circuit Size.

1.0.0.2 Learning

One of the main goals of the area of learning theory is to identify which learning problems are hard in the PAC-learning model. When PAC-learning a concept class \(\mathcal{C}\), we are given samples \((x,f(x))\) from a distribution \(\mathcal{D}\), where \(f\) belongs to \(\mathcal{C}\), and our task is to output with high probability a hypothesis \(c\) that approximates \(f\) well according to the distribution. If the output hypothesis \(c\) is in \(\mathcal{C}\), the learning algorithm is said to be proper, otherwise it is said to be improper. We also consider a semi-proper version of learning \(\mathcal{C}\)-circuits by \(\mathcal{C'}\)-circuits, where \(\mathcal{C'} \supseteq \mathcal{C}\).

It is known how to rule out even improper learning of various concept classes under cryptographic assumptions [18]–[20]. More recently, there has been exciting work on ruling out improper learning even of weak concept classes such as DNFs [21]–[23] based on average-case assumptions such as Feige’s hypothesis [24] and its variants. However, just as in the case of meta-complexity problems, showing hardness under worst-case assumptions remains challenging. This was explained in a work of Applebaum, Barak and Xiao [25], who showed that \(\mathsf{NP}\)-hardness of learning general Boolean circuits under Karp reductions or non-adaptive reductions would imply the collapse of the Polynomial Hierarchy. This leaves open the possibility of using more general reductions such as Turing reductions to show hardness.

Known worst-case hardness results are typically for proper learning of weak circuit classes such as DNFs, or for semi-proper learning where the output hypothesis class \(\mathcal{D}\) is not too much more powerful than the concept class [26]. While hardness of learning even restricted subclasses of monotone circuits under the uniform distribution is known under cryptographic assumptions [20], and unconditional hardness results are known in the statistical query learning framework [27], very little seems to be known about the worst-case hardness of learning monotone circuits.

As can be seen from the discussion above, there are several parallels between the situation with hardness of meta-complexity problems and the situation with hardness of learning. These parallels are not coincidental: learning for a circuit class \(\mathcal{C}\) can be seen as a search version of the problem of determining minimum \(\mathcal{C}\)-size of a Boolean function. Indeed, given access to a Boolean function \(f\), outputting a circuit of size \(s\) that computes \(f\) (perhaps approximately) via a learning algorithm witnesses that \(f\) has (perhaps approximate) circuit size at most \(s\). This connection is exploited to derive new learning algorithms in [15].

In this paper, we aim to establish strong results on the hardness of monotone learning based on worst-case assumption, and then to leverage the connection between monotone learning and meta-complexity to get strong inapproximability of monotone circuit size.

The meta-complexity problem we consider is the following: given \(m = \mathsf{poly}(n)\) labelled examples \((x_i, b_i)\), where each \(x_i\) is an \(n\)-bit string and \(b_i\) a bit, and a parameter \(s\), is there a monotone function \(f\) of monotone circuit size at most \(s\) that is consistent with the labelled examples, i.e., \(b_i = f(x_i)\) for each \(i\). In the context of learning, this is known as the Occam Learning problem, and the non-monotone analogue of this problem was called Partial Minimum Circuit Size Problem in [7], where it was shown to be \(\mathsf{NP}\)-hard. We are interested here in strong inapproximability results, which the techniques of [7] are incapable of proving, since they reduce from the well-approximable Set Cover Problem.

1.1 Our Results↩︎

Our first main result is on the hardness of PAC-learning monotone formulas. Proving hardness of improperly PAC-learning monotone formulas is at least as hard as showing \(\mathsf{NP}\)-hardness of learning general Boolean circuits, and hence beyond reach at this point in time. However, we are able to prove a strong result in the semi-proper setting under worst-case assumptions, where our concept class is the class of monotone formulas, but our hypothesis class is the class of polynomially larger monotone circuits. In this setting, we are able to get a quasipolynomial lower bound on the running time of any PAC-learning algorithm, assuming the randomised Exponential Time Hypothesis. Recall that the randomised Exponential Time Hypothesis (rETH) postulates that any algorithm solving 3SAT on formulas of \(n\) variables must take time \(2^{\Omega(n)}\). This is a standard hardness assumption in fine-grained complexity and parameterized complexity.

The formal statement of Theorem 1 is in the first item of Theorem 16 in Section 4.4. To the best of our knowledge, it was not known previously even how to get hardness of learning monotone circuits of size \(n\) by monotone circuits of size \(n^{1+\alpha}\) under standard worst-case assumptions. In fact, our techniques yield a tradeoff, where we can show hardness even for learning monotone formulas of even slightly super-polylogarithmic monotone formula size by monotone circuits of polynomial size. This result is stated in the second item of Theorem 16.

Our second main result shows the strong inapproximability of monotone circuit size for the partial version of the Minimum Monotone Circuit Size Problem, where we are given a sequence of labelled examples as input. The assumption used here is again rETH.

The formal statement of Theorem 2 is in the fourth item of Corollary 3.

Both Theorem 1 and Theorem 2 are consequences of a more general hardness result for a monotone version of the Computational Gap Learning problem studied in [25]. In our problem, which we call Monotone Circuit-Formula Gap Learning, we are given a circuit which samples a distribution of labelled examples \((x_i,b_i)\) where \(x_i\) is of length \(n\) and \(b_i\) a bit, and are asked to distinguish between 2 cases: the first where the distribution is completely consistent with a formula of size at most \(s_1\), and the second where the distribution does not even non-trivially correlate with any circuit of size at most \(s_2\). Here \(s_1, s_2: \mathbb{N} \rightarrow \mathbb{N}\) are parameters of the problem, which we are able to choose so that \(s_2 \gg s_1\). Theorem 1 follows immediately from our result about Monotone Circuit-Formula Gap Learning, while Theorem 2 follows by a standard sampling argument together with a union bound.

To show our central result about Monotone Circuit-Formula Gap Learning, we use a novel technique in the domain of hardness of learning: lifting, together with known strong inapproximability results for Resolution proof size [1], [28]–[31]. One of the main applications of lifting is to obtain monotone circuit size lower bounds in a generic way from Resolution proof width lower bounds [32], [33]. The generic nature of these reductions opens the possibility of using them to derive reductions from approximating proof size for various proof systems to approximating circuit size for various circuit models. This is yet another instance of the connection between learning and automatability of proof systems proposed in [26].

It may be useful to compare our results with the work of Hirahara [11]. Hirahara shows that a variant of the Computational Gap Learning problem is \(\NP\)-hard (under randomised reductions), where the task is to distinguish between linear programs (Turing machines computing a linear function) of size \(s_1\) and programs of size \(s_2 = s_1 \cdot n^{o(1)}\). Besides the obvious difference that we consider monotone circuits vs. formulas whereas [11] considers programs, crucially our results allow for a superpolynomial gap between circuit size, whereas [11] obtain only a sublinear gap between program size (though under the weaker assumption of \(\NP\)-hardness). Hirahara also shows \(\NP\)-hardness of approximating partial circuit size, when one is given the entire truth table of a partial function (referred to as \(\MCSP^*\)), again only with a \(n^{o(1)}\) approximation gap. In 2, however, we consider a succinct version of this problem, in which we are only given inputs where the function is defined; we also obtain a stronger hardness of approximation gap here.

We next give a technical overview of the ideas behind our proofs.

1.2 Technical Overview↩︎

1.2.0.1 Overall approach

The main insight of the paper is to convert the hardness of automating Resolution [1] into the hardness of approximating monotone circuit size, using results from the literature (called lifting theorems) that connect the complexity of Resolution refutations with the monotone complexity of Boolean functions [32].

To understand how this works, let us review how the seminal paper of Atserias and Müller [1] proved that automating Resolution is \(\NP\)-hard. Recall that an algorithm that automates Resolution must, given as input an unsatisfiable CNF formula \(\phi\), construct a Resolution refutation of \(\phi\) in time \(\poly(\abs{\phi} + s)\), where \(s\) is the size of the shortest Resolution refutation of \(\phi\). Given a 3-CNF formula \(F\) on \(n\) variables as input, the proof of [1] consists in constructing in polynomial-time a formula \(\REF(F)\) with the following properties:

1. If \(F\) is satisfiable, then \(\REF(F)\) admits a polynomial-size Resolution refutation;

2. If \(F\) is unsatisfiable, then any Resolution refutation of \(\REF(F)\) must have size \(2^{n^{\Omega(1)}}\).

In turn, this implies that if we can automate Resolution, then we can determine in which of the two cases we are in, and thus decide the satisfiability of \(F\).

Another significant ingredient in our approach is the DAG-like lifting theorem, which converts Resolution width lower bounds for a formula \(\phi\) into monotone circuit size lower bounds for a related monotone function \(f_{\phi}\) [32]. Importantly, the monotone complexity of the resulting function \(f_{\phi}\) is tightly connected to the Resolution width of \(\phi\), so that \(f_{\phi}\) has large monotone complexity iff \(\phi\) requires large Resolution width.

Ideally, we would now like to combine the properties of \(\REF(F)\) with the lifting theorem to reduce the satisfiability of \(F\) to deciding the monotone complexity of \(f := f_{\REF(F)}\) when given access to some succinct representation of \(f\) (e.g., access to random samples of \(f\), or a succinct representation of its truth-table). Unfortunately, the connection between monotone complexity and Resolution goes only via Resolution width, whereas the complexity gap obtained by Atserias-Müller is only for Resolution size. Though Resolution size does indeed give upper bounds on the monotone complexity of a related function via feasible interpolation [34]–[36], the converse is not known to hold.

A potential way out would be to consider the notion of block-width of proofs [1], a generalisation of Resolution-width to the setting when the variables are split into blocks, as is the case with \(\REF(F)\). The proof of Atserias-Müller can be rephrased as first showing that the block-width of \(\REF(F)\) is \(O(1)\) when \(F\) is satisfiable, and \(n^{\Omega(1)}\) when \(F\) is unsatisfiable [29]. However, though the notion of block-width can be lifted to Resolution size, it’s not known if it can be lifted to monotone circuit size, and indeed significant technical challenges have been found when trying to do so in at least one previous work [29].

A more promising approach comes from considering a different encoding of \(\REF(F)\) found in [28]. Their encoding admits a Resolution-width gap of \(\REF(F)\) of the following form¹:

1. If \(F\) is satisfiable, \(\REF(F)\) has Resolution-width \(O(n)\);

2. If \(F\) is unsatisfiable, \(\REF(F)\) has Resolution-width \(\Omega(n^3)\).

This seems to be what we are aiming at: an efficiently constructible formula with a noticeable gap in Resolution-width. However, lifting gives us that the monotone complexity of \(f_{\phi}\) is roughly \(2^{\Theta(\wRes(\phi))} \cdot \Res(\phi)\). So we obtain a function on \(n^{O(1)}\) input bits with \(2^{O(n)}\) monotone complexity when \(F\) is satisfiable, and \(2^{\Omega(n^3)}\) when \(F\) is unsatisfiable. Unfortunately, it is not clear how to distinguish between these two cases other than by guessing the exponential size circuit that computes the function. In other words, we have obtained a reduction from an \(\NP\) problem to an \(\NEXP\) problem, which is hardly surprising. Moreover, the reduction is ultimately useless, as we could just solve \(\SAT\) directly in exponential time.

We overcome this hurdle by constructing a different formula \(\REFx(F)\) with the following properties:²

1. \(\REFx(F)\) has \(2^{O(\sqrt{n})}\) variables and \(2^{O(\sqrt{n})}\) clauses.

2. \(\REFx(F)\) admits Resolution proofs of depth at most \(O(\sqrt{n})\) when \(F\) is satisfiable;

3. \(\REFx(F)\) requires Resolution proofs of width at least \(2^{\Omega(\sqrt{n})}\) when \(F\) is unsatisfiable.

Note that we obtain not just a Resolution width upper bound in the satisfiable case, but the strictly more powerful upper bound on Resolution depth, which is strongly tied to the size of monotone formulas [37], [38]. This is how we obtain a gap between monotone formula and circuit sizes in the final result. Note moreover that the resulting formula has subexponential size. This is a careful tradeoff that we exploit: by increasing the size of the formula, we are able to reduce its Resolution-width (and even its Resolution-depth). We now describe the construction of the formula in more detail.

1.2.0.2 The \(\REF^*(F)\) Formula

The formula \(\REF(F)\) essentially encodes the statement “\(F\) has a Resolution proof of small size \(s\)”, where \(s\) is a fixed polynomial in the number of variables of \(F\). When \(F\) is satisfiable, the formula \(\REF(F)\) is unsatisfiable, and this formula can be refuted with low block-width [1], [39].

Their strategy can be seen as low memory technique to achieve the following. Given any proposed proof for \(F\), a refuter³ navigates through it while maintaining the guarantee that the current clause is unsatisfied by the known satisfying assignment \(x^*\). Beginning at \(\bot\), eventually such a refuter will make it to a line of the proof that is a weakening of an axiom. Since the line must be unsatisfied by \(x^*\), it cannot be a weakening of any axiom and a contradiction has been found. While this technique can be used to show an \(O(1)\) block-width upper bound, the depth of the proof strategy is \(\Omega(s \cdot n)\), since it will involve learning every variable of \(\Omega(s)\) lines of the proposed proof. Adapting this technique to achieve a \(\sqrt n\) depth upper bound seems like a nearly hopeless endeavour on first blush. Achieving depth \(\sqrt{n}\) requires us to refute \(\REF(F)\) while querying in total fewer variables than the number of variables of \(F\). This presents two barriers:

• The refuter needs to get to a line of the proof that is claimed to be a weakening of an axiom while only seeing variables from \(\sqrt n\) total blocks, and

• The refuter needs to learn some information about all \(n\) variables while being able to query far fewer than \(n\) variables.

To overcome the first of these issues, we can force the proof to have depth \(\sqrt n\), as done in [30]. However, if we are only resolving over one literal at a time, the clauses at depth-\(\sqrt{n}\), which are weakening of axioms of \(F\), would have width \(\sqrt{n}\). This would break the lower bound of Atserias and Müller because their strategy requires that the clauses in the purported proof that are claimed to be a weakening of an axiom must have width \(n\).

To retrieve the lower bound, we can change the underlying proof system to one which resolves on \(\sqrt{n}\) variables at a time. This results in each block, instead of having just a left and a right child—which are the two clauses from which it was derived—now having \(2^{\sqrt{n}}\) children, and thus having one pointer \(\point_z\) for each possible setting \(z \in \bit^{\sqrt n}\) of the variables being resolved over (we also importantly fix the order in which variables are resolved over, with the first segment of \(\sqrt n\) variables, then the second segment, etc). Unfortunately, this immediately means that the resulting \(\REF(F)\) formula will have to be of size at least \(2^{\sqrt n}\) just to manage these pointer variables. On the positive side, this gives us a hint for how to overcome the second barrier.

In standard resolution refutations, if you know that a clause \(B'\) is the left child of \(B\) which is the result of resolving over \(x_i\), you know that \(x_i\) is in \(B'\), and more importantly that \(\lnot x_i\) is not in \(B'\); and if \(B'\) is the right child you know that \(\lnot x_i\) is in \(B'\), and more importantly that \(x_i\) is not in \(B'\). Consequently, knowing that \(x^*\) is a satisfying assignment, if the prover always queries whichever child is not satisfied by \(x^*\), they will eventually find themselves in a leaf which cannot be a valid weakening. In our new multi-variable resolution system, if you know that \(B'\) is the \(z\)^th child of \(B\), you know \(\sqrt{n}\) bits of information about the clause that \(B'\) claims to have. Using \(x^*\) as above, one could in principle get to a leaf which cannot be a valid weakening in depth \(O(\sqrt n)\).

We can extend this density of information from the pointers to a new class of summary variables \(\mathsf{summ}^B_{i,z}\) which give us information about all the variables from \(x_{(i-1)\sqrt{n}}\) to \(x_{i\sqrt{n}-1}\). This idea of using summary variables appeared before in [31]. It is important that our summary variables encode which literals are not present (which is ultimately what we are concerned with for the upper bound). Formally, \(\summlit_{i,z}^{B}\) is set equal to \(1\) to indicate that for each \(z_j = 1\), literal \(x_{(i-1)\formuladepth + j}\) is not present in block \(B\), and that for each \(z_j = 0\), literal \(\lnot x_{(i-1)\formuladepth + j}\) is not present in block \(B\). We can ensure that a Prover can learn what all \(\sqrt{n}\) of the \(\summlit_{i,z}^{B}\) variables for a leaf node should be while only querying the right set of \(O(\sqrt{n})\) variables on their way from the root to a leaf. To make our bounds as tight as possible, we add some additional complexity, including binary pointers for axioms, split variables to reduce clause width, and a low degree expander between each layer of the proof. This low-degree expander, which was previously used in [30], [31], allows us to keep down to a constant the number of \(\point_{B',z}^B\) variables a prover needs to query for each \(B,z\) before finding one that is set to one. While the expander does somewhat complicate the proof of the lower bound, we are able to derive it by reducing the retraction pigeonhole principle (rPHP) instance to finding a violated clause, similarly to what was done in [30].

1.2.0.3 Hardness of approximating circuit size and learning

To see how to join our new \(\REF^*\) formula with a lifting theorem to obtain the claimed hardness results, it will be helpful to understand the function that comes from lifting. Roughly speaking, “lifting” usually consists in composing some original computational object (e.g., a propositional formula or a function) with a gadget, so as to hide the original object in a stronger computational model in such a way that the only way to compute/solve the composed problem is by solving the original problem.

In our case, given a formula \(F\) with \(n\) variables and width \(k\), together with a parameter \(m\), the lifted function \(f := f_{F,m}\) from [32] will have \(\card{F} \cdot m^k\) input bits, where \(\card{F}\) is the number of clauses of \(F\). To each \(i \in [\card{F} \cdot m^k]\), we associate a pair \((C, \alpha)\), where \(C\) is a clause of \(F\) and \(\alpha \in [m]^k\). We interpret \((C, \alpha)\) as the \(k\)-width clause over the variables \(\set{y_{ij} : i \in [n], j \in [m]}\) obtained by replacing the variable \(x_i \in \vars(C)\) in \(C\) with \(y_{i, \alpha(i)}\). We can thus see each input to \(f\) as a collection of clauses \((C,\alpha)\). The task of the partial function \(f_{F,m}\) is to distinguish between the following two cases:

1. Accept (Output 1): there exists \(x : [n] \to [m]\) such that the input bit corresponding to \((C,x^{\vars(C)})\) is set to 1 for every clause \(C\) of \(F\), and everything else is set to 0;

2. Reject (Output 0): there exists \(y \in \blt^{mn}\) such that all input bits associated with clauses \((C,\alpha)\) satisfied by \(y\) are set to \(1\), and everything else is set to 0.

The partial function is clearly well-defined, as in the first case the collection of clauses is unsatisfiable, and in the second case they are satisfiable. For this same reason, no input to the function which contains all the clauses of Case (1) will ever be in Case (2), so the function is monotone. One can think of the function \(f\) as “hiding” several variable renamings of the the formula \(F\) in its input bits; to compute \(f\) is to “sniff out” if \(F\) has been completely embedded among the renamed clauses.

Most importantly for our purposes, we can easily sample from the distribution which half of the time gives a uniform accepting input of \(f\), and in the other half gives a uniform rejecting input. Indeed, first sample a bit \(b \in \blt\), then, if \(b = 1\), sample \(n \log m\) bits and interpret it as \(x : [n] \to [m]\), otherwise sample a string \(y \in \blt^{mn}\). With \(x\) (resp. \(y\)), it’s then easy to set the relevant bits so as to output an accepting (resp. rejecting) input of \(f_{F,m}\). Let us abuse notation and denote by \(\cald^{F,m}\) both a circuit that samples from this distribution of binary strings (together with the bit \(b\) as a prefix) and the distribution itself. We thus see samples from \(\cald^{F,m}\) as a pair \((x,b)\) where \(x \in \blt^{\card{F} m^k}\) and \(b \in \blt\). Given \(F\) and \(m\) as input, it’s also easy to see that we can construct the circuit sampling from \(\cald^{F,m}\) in time \(\poly(\card{F}, m^k)\).

Going back to the approach above, given an input \(F\) to 3SAT, our reduction will first construct \(\cald := \cald^{\REF^*(F), m}\), so as to obtain a distribution with the following properties. If \(F\) is satisfiable, then \[\label{eq:sat-case} \text{ there is a monotone formula L of size \leq s_1 s.t. L(x)=b for every (x,b) \in \supp(\cald); }\tag{1}\] if \(F\) is unsatisfiable, then \[\label{eq:unsat-case} \text{ every monotone circuit K of size \leq s_2 satisfies \Pr_{(x,b) \flws \cald}[K(x) = b] < 1/2+\gamma. }\tag{2}\] The value of \(s_1\) is \(2^{O(\sqrt{n} \log m)}\), and the value of \(s_2\) is \(2^{\Omega(m / \sqrt{n})}\); these come from a refined version of the DAG-like lifting theorem [40] with “small gadgets” that allows us to essentially pick any value of \(m\) we would like. However, lifting theorems typically are only stated for \(\gamma = 1/2\) (corresponding to a worst-case lower bound). Fortunately, generalising to \(\gamma \approx m^{-1}\) is an easy task, requiring only the modification of certain numbers and parameters in the proof of [40]. This is essential for our purposes, as in a learning problem we only expect to approximate the target concept.

We are now ready to state the computational problem for which we show a lower bound. The Monotone Circuit-Formula Gap Learning problem \(\mCFGL_{s_1}^{s_2}[\gamma]\) is the problem of distinguishing between cases \((\ref{eq:sat-case})\) and \((\ref{eq:unsat-case})\) when given \(\cald\) as input. Given that our \(\REFx(F)\) formula has size \(2^{O(\sqrt{n})}\), the reduction from SAT to this problem takes this time. Under ETH, we thus obtain an \(N^{\Omega(\log N)}\) lower bound for this problem, since the size \(N\) of the input is \(2^{O(\sqrt{n})}\). To reduce to the case \(s_1 = n\), we pad the sampled strings; this takes time \(2^{\tld{O}(\sqrt{n})}\), so our final lower bound is \(N^{\tld{\Omega}(\log N)}\).

We can further reduce this problem to a gap version of Partial-Monotone-MCSP we call \(\mMCFSP_{s_1}^{s_2}[\gamma]\)⁴. In this problem, instead of \(\cald\), the algorithm is given \(t\) examples \((x_1,b_1), \dots, (x_t,b_t)\), and must distinguish whether there is a monotone formula \(L\) of size \(s_1\) such that \(L(x_i) = b_i\) for all \(i \in [t]\), or whether every monotone circuit \(C\) of size \(s_2\) is such that \(\card{\set{i \in [t] : C(x_i) \neq b_i}} \geq (1/2+\gamma)t\). The reduction is randomised, naturally coming from sampling the distribution \(\cald\). Moreover, we need to sample \(O(s_2 \log s_2)\) examples so that, with high probability, any circuit of size at most \(s_2\) will err on a proportion larger than \(1/2+\gamma\) of the examples (in case (2 )), and so the reduction takes time \(O(s_2 \log s_2)\). This means that we get a tradeoff between the choice of \(s_2\) and the runtime lower bound coming from rETH. The same reduction also gives us lower bounds on PAC-learning.

2 Preliminaries↩︎

For \(f,g : \bbn \to \bbn\), we write \(f \sim g\) if \(\lim f/g \to 1\), and \(f \asymp g\) if \(f = \Theta(g)\). We say that a function Boolean \(f\) is \(\gamma\)-approximated by \(g\) over a distribution \(\cald\) if \(\Pr_{x \flws \cald}[f(x)=g(x)] \geq 1/2+\gamma\).

2.1 Basic Complexity↩︎

Monotone circuits are Boolean circuits without \(\neg\) gates. Formulas are Boolean circuits whose gates have fan-out 1. Monotone formulas are analogously defined.

The Exponential-Time Hypothesis (ETH) postulates that there exists a constant \(\eps > 0\) such that any algorithm solving 3SAT on \(n\)-variate formulas must take time \(2^{\eps n}\). The randomised ETH (rETH) postulates the same lower bound for randomised algorithms.

2.2 Expander Graphs↩︎

A \((m,n,\delta,r,e)\)-bipartite expander graph is a bipartite graph \(\graph=((U\cup V), E)\) with \(|{U}| = m\), \(|{V}| = n\), with every vertex in \(U\) having degree at most \(\delta\), and where for every subset \(S\subseteq [m]\) such that \(|S|\leq r\), the neighbourhood of \(S\), denoted \(N(S)\), satisfies \(|{N}(S)|\geq e|S|\).

A standard calculation [41] shows that random graphs are good expanders. We record one parameter regime that we use in our applications.

2.3 Proof Complexity↩︎

2.3.0.1 Resolution

A literal is a propositional atom or its negation, a clause is a disjunction of literals, and a CNF formula is a conjunction of clauses. We see clauses as sets of literals, and write simply \(C \subseteq D\) to express that \(C\) is a subclause of \(D\). We denote the set of variables in a clause \(C\) by \(\vars(C)\) (if \(x_i\) or \(\neg x_i\) are present in \(C\), we have \(x_i \in \vars(C)\)). A Resolution refutation of an unsatisfiable CNF formula \(\varphi = C_1 \land \dots \land C_m\) over variables \(x_1, \dots, x_n\) is a sequence \(D_1, \dots, D_s\) of clauses over \(x_1, \dots, x_n\) such that \(D_s = \bot\), denoting the empty clause, and for every \(i \in [s-1]\), the clause \(D_i\) either (a) is one of the clauses \(C_1, \dots, C_m\) of \(\varphi\), or (b) is a weakening of a previous clause, meaning that \(D_i \supseteq D_j\) for some \(1\leq j < i\), or (c) has been obtained from two previous clauses \(D_j = A \lor x\) and \(D_k = B \lor \neg x\), for \(j, k < i\), by an application of the Resolution rule:

We say that \(A \lor B\) was obtained by resolving over \(x\). The size of the refutation is \(s\), the number of clauses appearing in the refutation.

To every Resolution refutation we can associate a directed acyclic graph (dag) in a natural way. We define the depth of the proof as the length of the longest path in the dag, starting from the root labeled by the empty clause \(\bot\). The proof is said to be tree-like if the associated graph is a tree rooted at \(\bot\).

Let \(F\) be an unsatisfiable \(k\)-CNF formula. We denote by \(\wRes(F)\) the minimum integer such that \(F\) admits a Resolution refutation whose clauses all have width at most \(\wRes(F)\). Let \(\ResDepth(F)\) be the minimum integer such that \(F\) admits a Resolution refutation with depth at most \(\ResDepth(F)\). We denote by \(\Res(F)\) the size of the smallest Resolution refutation of \(F\), and by \(\TreeRes(F)\) the size of the smallest tree-like such refutation. We denote by \(\card{F}\) the number of clauses in \(F\).

2.3.0.2 Prover-adversary game

An equivalent characterisation of Resolution width and Resolution depth can be given by notions from query complexity. Suppose that \(F\) is an \(n\)-variate unsatisfiable CNF formula. Given any assignment \(x \in \blt^n\) to the variables of \(F\), some clause of \(C\) is necessarily falsified. The minimum number \(k\) of queries to the variables of \(F\) needed to discover one such clause is equivalent to \(\ResDepth(F)\).

To characterise \(\wRes\), it is helpful to modify the above setup in what is commonly called a “Prover-Adversary game”. As before, the Prover is querying variables, but now the Prover is allowed to forget the value of some queried variables. The adversary is answering the queries, but may respond with different values when a variable whose value was forgotten is queried again. The minimum number \(k\) of variables that the Prover needs to store in order to discover a falsified clause is equal to \(\wRes(F) \pm 1\) [42].

2.4 Lifting for Average-Case Lower Bounds↩︎

Given a gadget \(g : \calx \times \caly\), let \(g^n : \calx^n \times \caly^n\) denote the function \[g^n(x,y) = (g(x_1,y_1),\dots,g(x_n,y_n)).\] Let \(\Ind_{m} : [m] \times \blt^m \to \blt\) denote the “index gadget”, defined as the Boolean function such that \(\Ind_m(x,y) = y[x]\).

The following theorem shows that the monotone circuit complexity of \(f_{F,m}\) is roughly \(m^{\Theta(\wRes(F))}\) for some \(m \gg \wRes(F)\); moreover, a formula upper bound of the form \(m^{O(\ResDepth(F))}\) also holds. This result follows from (a small modification of) the so-called lifting theorem, which first appeared in [32], from which monotone circuit lower bounds follow from Resolution width lower bounds. We use the lifting theorem from [40], which builds on [43], [44], as it not only has better parameters, but also gives a lower bound for \(f_{F,m}\) for smaller values of \(m\), which is essential to our purposes.

We say that a circuit \(D : \blt^r \to \blt^N\) represents a distribution \(\cald\) over \(N\)-input bits if the random binary string \(D(\rndr)\) where \(\rndr \flws \blt^r\) is distributed according to \(\cald\).

3 Shallow Refutation Formula↩︎

Let \(F\) be a 3-CNF formula over \(n\) variables. The \(\REF_s(F)\) formula encodes the statement “\(F\) has a resolution proof of length \(s\)”. Slightly more formally, the variables of \(\REF_s(F)\) are divided into \(s\) blocks, each of which encodes a potential clause in the purported refutation of \(F\) and how this clause was derived, and the clauses of \(\REF_s(F)\) enforce that all derivation steps are sound.

The known resolution refutation of \(\REF_s(F)\) when \(F\) is satisfiable, given by Pudlák’s upper bound [39], has large width \(\Omega(n)\). Under ETH, a large width is unavoidable, since it is possible to find width \(w\) refutations of an unsatisfiable \(N\)-variate CNF formula in time \(N^{O(w)}\). While it is possible to show a gap between the Resolution width of the formula \(\REF_s(F)\) in the satisfiable and unsatisfiable cases of \(F\) [1], [28] (\(O(n)\) vs.\(\Omega(s/n)\)), for our applications we need a better upper bound. In this section, we define a formula related to \(\REF_s(F)\) which substantially decrease the width upper bound at the cost of an increase in the size of the formula. Moreover, we show that our new formula has small Resolution depth when \(F\) is satisfiable.

3.1 The New Formula \(\eREF_d(F)\)↩︎

Our new formula is denoted by \(\eREF_d(F)\), and it depends on a bipartite expander graph \(G\) and an integer parameter \(d\). We somewhat follow the notation established in “The Proof Analysis Problem” by Arteche et al. [45], but modify the structure of the purported resolution refutation and introduce some extension variables, similar to what was done in [30] and [31].

As was done in [30] we structure the blocks in \(\formuladepth\) layers (instead of \(n\)), and as in [31], we add “summary” variables that give information about segments of \(\noverdepth\) variables. These changes allow us to turn the \(O(1)\) block-width upper bound and corresponding \(O(n)\) resolution width upper bound in [39] into an \(O(\formuladepth)\) upper bound on depth, at the cost of increasing the number of variables and clauses in \(\eREF_d(F)\) to \(2^{\Theta(\noverdepth)}\).

Since it is crucial that these summary variables encode that literals are absent, we also switch focus and define “un-literal” variables encoding that single literals are not present in a block as opposed to previous encoding of \(\REF\) which has variables encoding the inclusions of literals. This is done only for exposition purposes since our \(\lit\) variables are just the negation of the usual literal variables. We also include binary variable for pointers (as done in [28]) to make it possible to query pointers more efficiently.

Finally, we also include “split” variables to turn our formula into a \(3\)-CNF formula using a standard transformation. This is done in order to minimise the blow-up in size of the function we obtain after lifting \(\eREF_d(F)\).

We start by explaining the structure of the formula \(\eREF_d(F)\). We then introduce the main variables of \(\eREF_d(F)\) and the clauses enforcing that the purported proof is sound and is structured as we would like. Finally, we introduce the split variables and explain how they are used to transform the formula into a \(3\)-CNF formula.

3.1.0.1 Structure of \(\eREF_d(F)\) and notation

Let \(F\) be a CNF formula over \(n\) variables and \(\poly(n)\) clauses, let \(d\) be an integer, and let \(G\) be a bipartite graph with \(t2^{n/d}\) nodes on left side, \(t\) nodes on the right, and outdegree \(\delta\) from each node on the left. We define \(s \mathrel{\vcenter{:}}= t \cdot d\). For the sake of convenience in our presentation, we assume that \(d\) divides \(n\), and that \(|F|\) (the number of clauses of \(F\)) and \(\delta\), the left outdegree of the expander \(G\), are powers of 2, so they can be cleanly indexed into by binary pointers. We later explain why we can make these assumptions without loss of generality (see 6).

Given an integer \(S\) which is a power of \(2\) and an integer \(X\in[S]\), we denote by \(\bin_S(X)\) the binary string of length \(\log S\) encoding \(X\). When \(S\) is clear from the context, we simply write \(\bin(X)\). For instance, for \(A \in [|F|]\), we write \(\bin(A) \in \bit^{\log |F|}\) to be the binary string of length \(\log |F|\) encoding \(A\).

The formula \(\eREF_d(F)\) is defined over \(s+1\) blocks arranged in \(d+1\) layers (see 1). The block \(s+1\) is the root and it is alone in layer \(0\). The other \(s\) blocks are arranged in decreasing order in layers \(1\) to \(d\) with \(s/d\) blocks per layer. Formally, for \(B \in [s]\), we have \(\layer(B) = 1+d - \lceil B/t \rceil\) while \(\col(B) = B - (\lceil B/t \rceil - 1)t\). So, for example, for block \(s\) we get that \(\layer(s) = 1, \col(s) = t\), while for block \(1\) we get \(\layer(1) = d, \col(1) = 1\).

The idea is that each block contains a clause: block \(s+1\) contains the empty clause, and blocks at layer \(i\) contain clauses over the first \(i\cdot \noverdepth\) variables. For this to locally look like a sound refutation, each block is supposed to have \(2^{\noverdepth}\) children on the layer below, one for each possible extension of the clause in the block to the next \(\noverdepth\) variables: for each \(z\in \{0,1\}^{\noverdepth}\), the clause in the \(z\)^th child of a block \(B\) should not be satisfied by assigning \(z\) these \(\noverdepth\) variables. The \(z\)^th child of a block is encoded by some variables so that, even though it is not possible to assign \(2^{\noverdepth}\) distinct children to each block, locally it can still look like the formula \(\REF^G_d(F)\) is consistent.

Finally, we would like there to be only a few possible options for each of the \(z\)^th children of a block. We use the graph \(G\) to determine these options: each node on the left-side of \(G\) corresponds to a \(z\)^th child of a block at layer \(i\in[d]\) and each node on the right-side of \(G\) corresponds to a block on layer \(i+1\). The neighbour relation corresponds to the possible blocks at layer \(i+1\) that could be the \(z\)^th child of a block at layer \(i\). To make our encoding more succinct, we need a way of managing binary indices for the at most \(\delta\) blocks \(B'\) that could be a \(z\)^th child of \(B\). To do this, we need a surjection (which we denote \(\sur_{z,\col(B)}\)) from the set of at most \(\delta\) valid blocks that can be the \(z\)^th child to \([\delta]\). It is easy to see that, if \(\sur_{z,\col(B)}\) is the lexicographical order over the valid blocks, then \(\sur_{z,\col(B)}\) can be efficiently computed when needed while constructing \(\REF^G_d(F)\) in all the parameter regimes considered in this paper. Note that there may be parameter regimes in which this is not the case.

3.1.0.2 The variables of \(\eREF_d(F)\)

Let \(x_1,..,x_n\) be the variables of \(F\). For any variable \(x_i\), the variable \((x_i)^0\) corresponds to \(\lnot x_i\) and \((x_i)^1\) corresponds to \(x_i\). We define the set \(\Lit_n = \{x_1,...,x_n,\overbar{x}_1,...,\overbar{x}_n\}\). Let \(\textsf{Leaves} \mathrel{\vcenter{:}}= [s/d]\) be the set of blocks at layer \(d\). Some variables (like \(\weak, \weak\bin\), which encode what axiom in \(F\) the block is a weakening of, in unary and in binary, respectively) are only defined for blocks in \(\textsf{Leaves}\) and some (\(\point,\point\bin\), which encode the blocks that were used to derive the current block, also in unary and in binary, respectively) are only defined for blocks that are not in \(\textsf{Leaves}\).

Recall that, in our setting, a block is obtained by resolving \(n/d\) variables at once. Therefore, the \(z\)^th child, for \(z\in \bit^{n/d}\), of a block at layer \(i\) should not contain literals \(x_{i\formuladepth + j}\) for each \(z_j = 1\), nor literals \(\lnot x_{i\formuladepth + j}\) for each \(z_j = 0\). This will be enforced by using the variables \(\summlit\). In fact, except for blocks that are leaves, the only information about what literals are contained in each block is given by these \(\summlit\) variables. Since the layer of a block determines what variables can be present in the block, only the relevant \(\summlit\) variables are defined for each block. In particular, the root does not contain any \(\summlit\) variable and the leaves contain all \(\summlit\) variables. Moreover, the leaves are the only blocks that contain the \(\lit\) variables, as only then are these needed to connect the clause in the block with the axiom of \(F\) that it is supposedly a weakening of.

We are now ready to introduce the variables of our formula.

We record two remarks regarding the variables of the formula. First, we note a bound on the number of variables.

Second, we observe that the divisibility assumptions mentioned earlier can easily be dropped.

3.1.0.3 The clauses of \(\eREF_d(F)\)

We first introduce the unsplit versions (i.e., of width possibly larger than \(3\)) of the clauses which make up \(\eREF_d(F)\). These clauses enforce the basic structure of the Shallow-Resolution formula ensuring particularly that our summary and pointer variables interact correctly. The clauses are defined for arbitrary \(G\) but in our proofs we focus on two cases for \(G\): either \(G\) is a bipartite expander with \(t\) nodes on the left side, \(t \cdot 2^{n/d}\) on the right side, and outdegree \(\delta\) from each node the left side; or \(G\) is a complete graph such that all \((\col(B), (\col(B'),z)) \in E(G)\).

We divide the clauses into three categories depending on whether the block in the superscript is in layer \(0\) (meaning the block is the root), in layer \(d\) (meaning the block is a leaf), or between layers \(1\) and \(d-1\) (meaning the block is an internal block).

3.1.0.4 Root case — final block is enabled

3.1.0.5 Leaf case — managing axioms

The following clauses are defined for each \(B\in \mathsf{Leaf}\).

3.1.0.6 Internal Step — pointer and summary enforcement

The following clauses are defined for each \(B\) that is not a leaf, i.e., for \(B\) such that \(\layer(B) < \formuladepth\); for each \(z\in \bit^{n/d}\); and for each \(B'\) which is a possible \(z\)th child for \(B\), i.e., for \(B' \in P_B \mathrel{\vcenter{:}}= \{B': \layer(B') = \layer(B)+1\) and \(((\col(B),z), \col(B')) \in E(G) \}\).

This completes the list of the clauses of the non 3-CNF version of the formula \(\eREF_d(F)\). We first observe that there are not too many clauses in this formula and that they are not too wide.

We now introduce a final set of variables which we refer to as “split variables”. These are used to transform the formula into \(3\)-CNF using a standard transformation. For every clause \(C_i = v^i_1 \lor v^i_2 \lor ... \lor v^i_{|C_i|}\) so far introduced, we introduce a collection of split variables \(\splitv_{C_i}^j\) for each \(j \in [|C_i| - 3]\) and replace \(C_i\) with a collection of clauses \((v^i_1 \lor v^i_2 \lor \splitv_{C_i}^1) \land (\lnot \splitv_{C_i}^1 \lor v^i_3 \lor \splitv_{C_i}^2) \land ... \land (\lnot \splitv_{C_i}^{|C_i|-3} \lor v^i_{|C_i| - 1} \lor v^i_{|C_i|})\).

We denote the formula after splitting by \(\eREF_d(F)\). Note that, by 7, if \(s = 2^{O(\noverdepth)}\), \(d\leq n\), \(|F| = n^{O(1)}\), and \(\delta = O(s)\) then before splitting, the formula has \(2^{O(\noverdepth)} \cdot n^{O(1)}\) clauses containing at most \(O(\log n + \log s)\) variables each. As a consequence, after splitting, \(\eREF_d(F)\) has at most \(O(\log n + \log s)\cdot2^{O(\noverdepth)} \cdot n^{O(1)}= 2^{O(\noverdepth)} \cdot n^{O(1)}\) clauses, each of which contains at most \(3\) variables. We record this observation below.

3.2 Main Theorem↩︎

We prove our main theorem for an arbitrary expander graph, and we then instantiate this theorem with two different graphs.

From 9 we obtain two corollaries. First, using the fact that an unbalanced complete bipartite graph is an expander (3), we obtain the following.

Using a randomised construction of expanders (1), we can improve the above construction in the following way.

4 Learning Lower Bounds Under ETH↩︎

In this section, we formally prove 1 2. We begin by defining a gap learning decision problem to which we reduce the SAT problem, and from which we are able to reduce to other learning problems.

We record an observation about the sampling circuit that we use later on.

We now implement the strategy outlined in the introduction. We take a 3-CNF formula \(F\) on \(n\) variables, construct the formula \(\eREF_d(F)\) satisfying either 1 (in case of a deterministic reduction) or 2 (in case of a randomised reduction). Using a deterministic reduction, taking \(m\) such that \(n \leq m \ll 2^{n/d}\), \(t \leq 2^{n/d}\) and \(\ell = \eps dm/n \ll 2^{t/n}\) for small enough \(\eps\) in 4 gives that the function \(f_{\eREF_s(F),m}\) has \(N = 2^{O(n/d)} \cdot n^{O(1)}\) input bits and the following monotone complexity:

1. At most \(m^{{O}(d\log t + \log n)} = 2^{O( (d\log t+\log n) \log m )}\) when \(F\) is satisfiable, and

2. At least \(2^{\Omega(\ell)} \geq 2^{\Omega(m/\log N)}\) when \(F\) is unsatisfiable.

Using a randomised reduction, the value of \(t\) is irrelevant and the resulting monotone complexity is

1. At most \(m^{{O}(d + \log n)} = 2^{O( (d+\log n) \log m )}\) when \(F\) is satisfiable, and

2. At least \(2^{\Omega(\ell)} \geq 2^{\Omega(m/\log N)}\) when \(F\) is unsatisfiable.

Since we are reducing from ETH, the value \(m = \poly(n)\) is already good enough, as a monotone circuit lower bound beyond \(2^{\Omega(n)}\) (for an \(N\)-variate function) is not of much use for reductions to Partial-MCSP or PAC-learning (since we would need to output a circuit of this size or generate an exponential number of examples). The value \(d\) is then the main parameter we choose. There are two parameter regimes we will care about:

1. (\(d = \log n\)). We obtain a formula upper bound which is smaller than the number \(N\) of input bits (a “junta”). The runtime lower bound based on ETH becomes \(N^{\Omega(\log \log N)}\).

2. (\(d \approx \sqrt{n}\)). This gives us a polynomial vs.quasipolynomial gap. The runtime lower bound becomes \(N^{\tld{\Omega}(\log N)}\).

4.1 ETH-hardness of Monotone Circuit-Formula Gap Learning↩︎

We first show the result for juntas.

The result for polynomial vs.quasipolynomial gap follows similarly.

4.2 rETH-hardness of Monotone Circuit-Formula Gap Learning↩︎

Next, we show slightly stronger versions of these results but under rETH.

4.3 From Gap Learning to Partial-Gap-MCFSP↩︎

We now define the partial MCSP problem we consider. Instead of the entire truth table of a partial function, we consider a more succinct encoding where we are only given locations where the function is defined.

To show hardness of \(\mMCFSP\), it suffices to reduce from \(\mCFGL\). As described in the introduction, it suffices to sample from the distribution \(\cald\) given as input to \(\mCFGL\). In the small formula case, we clearly generate examples which can be computed by a small formula. In the large circuit case, with enough examples we can conclude by the Chernoff inequality that no circuit of small size can compute most of those examples correctly.

We now employ the hardness results obtained for \(\mCFGL\) under rETH in 4.2 to obtain hardness of \(\mMCFSP_{s_1}^{s_2}\) using the reduction of the previous theorem. We consider 4 choice of parameters which are in a way best possible:

1. Junta vs.quasipolynomial. Here we take the largest gap possible between formula and circuit size. This gives us a weaker runtime lower bound of \(N^{\Omega(\log \log N)^{1-\eps}}\). This is the weakest runtime lower bound we obtain.

2. Linear vs.quasipolynomial. Here we obtain a weaker gap but against superpolynomial-size circuits. This gives us a better runtime lower bound of \(N^{\Omega(\log N)^{1-\eps}}\).

3. Junta vs.polynomial. We then consider the setting where the gap is largest possible subject to \(s_2 = \poly(n)\). This gives us a runtime lower bound of \(N^{\Omega(\log \log N)}\), slightly better than (1).

4. Linear vs.polynomial. We weaken the gap to an arbitrary polynomial \(n^c\). This gives us a better runtime lower bound of \(N^{\Omega(\log N)}\), slightly better than (2). This is the strongest runtime lower bound we obtain.

We obtain the following result for each of these parameter regimes.

4.4 From Gap Learning to Improper PAC-Learning↩︎

Finally, we explain how to obtain hardness of PAC-learning. We first define formally the notion of PAC-learning. Given a function \(f : \blt^n \to \blt\) and a distribution \(\cald\) with support in \(\blt^n\), we denote by \(\Ex(f,\cald)\) the oracle that runs in unit time and outputs a sample \((x,b)\) where \(x \flws \cald\) and \(b = f(x)\). We also define \(\err_{f, \cald}(h) := \Pr_{x \in \cald}[h(x) \neq f(x)]\).

For \(s : \bbn \to \bbn\), let \(\calc_{s(n)}\) (resp. \(\call_{s(n)}\)) be the set of monotone Boolean circuits (resp. formulas) on \(n\) bits of size \(s(n)\). Let \(\calc_s = \bigcup_{n \in \bbn}\calc_{s(n)}\) and \(\call_s = \bigcup_{n \in \bbn}\call_{s(n)}\). Hardness of PAC-learning \(\call_s\) by \(\calc_s\) follows from the results of 4.2 by a proof similar to the one employed in the previous section.

Acknowledgements↩︎

We thank Noel Arteche for helpful discussions, and the anonymous reviewers for their valuable comments and suggestions. Rahul Santhanam and Bruno Cavalar acknowledge support from the EPSRC project EP/Z534158/1 on “Integrated Approach to Computational Complexity: Structure, Self-Reference and Lower Bounds”. Bruno Cavalar also acknowledges support of the UK Research and Innovation (UKRI) through an EPSRC Postdoctoral Fellowship (grant ref. UKRI3441). Susanna F. de Rezende was supported by the Knut and Alice Wallenberg Foundation grant KAW 2023.0116, ELLIIT, and the Swedish Research Council grant 2021-05104.

5 Proof Sketch of the Refined Lifting Theorem↩︎

Throughout this appendix, we assume familiarity with the notation and definitions from the paper [40]⁵. 4 is proved in [40] only for the case when \(\gamma = 1/2\). However, it is straightforward to extend it to the case \(\gamma \geq 2m^{-(1-\delta)}\) at the expense of only a slightly weaker size lower bound, that is, of showing that the protocol is of size at least \(m^{(1-\delta)(\ell -1)}\) (instead of \(m^{(1-\delta)}/2\)). Here \(\delta\) is the same parameter as in [40], that is, \(\delta\) such that \(m^\delta = 2K\cdot |\Sigma| \cdot 4\ell \cdot \log(2mN^2)\) for \(K\) being the constant given from the Full Range Lemma. Note that in our case \(\Sigma = \{0,1\}\). Moreover, observe that \(m^\delta \leq c' \ell \log(mN)\) for a large enough absolute constant \(c'\), and so, in particular, we will be proving the statement for \(\gamma \geq 2 c' \ell \log(mN)/m \geq 2m^{-(1-\delta)}\).

Suppose that some small circuit has \(1/2+\gamma\) correlation with \(f\). This implies that the root rectangle \(R=R^X \times R^Y\) obtained from the circuit has density at least \(\gamma\) in both sides (instead of density \(1\), as in [40]). Suppose that the DAG has size at most \(m^{(1-\delta)(\ell -1)} \leq m^{(1-\delta)\ell} \cdot \gamma/2\), This changes the density of both the \(X\)-error and of the \(Y\)-error accumulated at the root to be at most \(\gamma/2\) (instead of at most \(1/2\)), and, therefore, the root rectangle, with errors removed, has density at least \(\gamma/2\) in both sides. This only affects the argument that \(R^X \times (R^Y \setminus Y^R_{\err})\) is a \(\star^N\)-(pre-)structured rectangle, that is, that \(R^X\) is \(\star^n\)-predense and \(|R^Y \setminus Y^R_{\err}|\geq 2^{mN-4\ell \log mN}\) (since in our case \(\Sigma = \{0,1\}\)).

We first argue that \(R^X\) is \(\star^N\)-predense. Indeed, for any \(\emptyset \neq I \sseq X\) the min-entropy of \(R^X_I\) is at least \[\begin{align} \card{I} \log m - \log(2/\gamma) &= \card{I} \log m - (1-\delta)\log m \\&\geq \card{I} \log m - (1-\delta) \card{I} \log m \\&\geq \delta \card{I} \log m. \end{align}\] We have thus obtained the bound required to conclude that \(R^X\) is \(\star^N\)-predense.

It remains to show that \(|R^Y \setminus Y^R_{\err}|\geq 2^{mN-4\ell\log mN}\). This follows easily since \(|R^Y \setminus Y^R_{\err}|\geq 2^{mN} \cdot \gamma / 2\) and \(\gamma/2 = m^{-(1-\delta)} \geq 2^{-\log m} \geq 2^{-4\ell\log mN}\). We therefore conclude that \(R^X \times (R^Y \setminus Y^R_{\err})\) is a \(\star^N\)-(pre-)structured rectangle, and the rest of the proof is the same.

This implies the size of lower bound of \(m^{(1-\delta)(\ell-1)} \geq (m/c'\ell \log(mN))^{\ell-1}\) for any \(\gamma \geq 2 c' \ell \log(mN)/m\). Choosing the absolute constant \(c = 2c'\) gives us 4.

6 Proof of the Lower Bound for the Refutation Formula↩︎

In this appendix, we prove [it:thm-extended-ref-unsat] of 9, that is, we show that if \(F\) is unsatisfiable \(3\)-CNF formula over \(n\) variables, with \(\poly(n)\) clauses, \(d \leq n\) and \(t \leq 2^{\noverdepth}\), and \(\graph\) is a \((\blockslayer\cdot\pointersblock,\blockslayer,\delta,r,c)\)-bipartite expander graph, then \(\eREF_d(F)\) requires Resolution proofs of width at least \(2^{\Omega(r(c-1)/n)}\). The proof follows along the same lines of the ones in [28] and in [30].

6.1 Weak Graph \(\PHP\) Formula↩︎

The formula we use is a graph version of the retraction pigeonhole principle, \(\PHP\) [46], [47]. The retraction pigeonhole principle was also used in [28] to prove a similar reduction.

In this variant of the pigeonhole principle, the pigeon-mapping is restricted to the edges of a given bipartite graph and, moreover, there is an efficient way to invert the mapping. Formally, given a bipartite graph \(\graph = (U \disjointunion V, E)\) with \(U=[m]\) and \(V=[n]\), and an arbitrary family of surjections \(\mathsf{sur}_i : [\delta] \rightarrow N(i)\) for each \(i\in [m]\), the variables of the formula \(\PHP(\graph)\) describe two functions, \(f\colon [m]\to[\delta]\) and \(g\colon[n]\to[m]\), as follows.

• Pigeon map variables. For every pigeon \(i\in[m]\) there are variables \(f_{ik}\), \(k \in [\log \delta]\). The pigeon map variables encode in binary a hole \(\mathsf{sur}_i(f(i)) \in N(i)\) that is expected to house pigeon \(i\).

• Hole map variables. For every hole \(j\in [n]\) there are variables \(g_{j\ell}\), \(\ell\in [\log m]\). These variables encode in binary a pigeon \(g(j)\in[m]\) that is expected to occupy hole \(j\).

The axioms of \(\PHP(G)\) state that for every \(i\in[m]\) and \(j\in N(i)\), \[\label{eq:invertible-gphp-functional-notation} \enspace \mathsf{sur}_i(f(i)) = j\enspace \Longrightarrow \enspace g(j) = i \,.\tag{4}\] Note that (4 ) corresponds to \(\log m\) clauses each of width \(\delta\). Therefore, \(\PHP(\graph)\) can be written as an \(O(\delta)\)-width CNF formula with \(O(n\delta \log m)\) clauses.

It was shown in [48] that if \(\graph\) is a good enough expander, then the pigeonhole principle formula over \(\graph\) requires large width to be refuted in resolution. As argued in [40], we can obtain the following, slightly stronger, lower bound on the width required to refute the pigeonhole principle formula over \(\graph\), which in particular applies to our encoding \(\rPHP(\graph)\).

In particular, this implies that if \(\graph\) is an \((m,n,\delta,r,\delta/2)\)-bipartite expander graph from 1 then \(\wRes(\rPHP(\graph)) = \Omega(\sqrt{n})\). And if \(\graph=((U\cup V), E)\) is a complete bipartite graph with \(|{U}| = m\), \(|{V}| = n\), then by 3 \(\wRes(\rPHP(\graph)) \geq n/4\).

6.2 Decision Tree Reductions↩︎

Our goal is to show, via a moderately small-depth reduction, that the width required for refuting \(\myRef(F)\) is almost as large as the width required for refuting \(\PHP(\graph)\). For the definition of reduction, we view a clause as a function, that is, given a CNF formula \(H\) over \(m\) variables, we view a clause \(\clause\in H\) as a function from \(\{0,1\}^m\) to \(\{0,1\}\), which can be computed by a depth-\(|\clause|\) decision tree. In this way, given a function \(\redfun : \{0,1\}^n \rightarrow \{0,1\}^m\), \(\clause\circ \redfun\) is a function from \(\{0,1\}^n\) to \(\{0,1\}\). Moreover, if \(\redfun_i\) is computed by a depth-\(d\) decision tree, then \(\clause\circ \redfun\) can be naturally written as a (\(d\cdot |\clause|\))-CNF formula (i.e., a CNF formula with width \(d \cdot |\clause|\)) over \(n\) variables.

The important property of reductions that we use is that width bounds carry over.

For the rest of this section, we let \(\graph\) be a \((\blockslayer\cdot\pointersblock,\blockslayer,\delta,r,c)\)-bipartite expander graph, where \(\blockslayer \leq \pointersblock\). Combining 17 and 2 implies that, in order to obtain the lower bound in 9, it is enough to show that \[\label{eq:php-shref} \PHP(\expandergraph)~\leq_{O(n)}~\myRef(F) \,.\tag{5}\]

6.3 Overview of the Reduction↩︎

The proof of the reduction is similar to that of [30] which in turn follows the one in [28]. As in [30], the reduction is guided by a full tree \(\calt\) of height \(\formuladepth\) and arity \(\pointersblock\). Recall that we consider a fixed ordering of the variables of \(F\). Each node of \(\calT\) contains a clause. The root contains the empty clause (\(\bot\)) and each node at distance \(\alpha\) from the root contains a clause with \(\alpha n/d\) defined recursively as follows. If a non-leaf node at distance \(\alpha\) from the root contains a clause \(C\) using the first \(\alpha \noverdepth\) variables, each of its \(\pointersblock\) children contains one of the possible weakenings of \(C\) to the next \(\noverdepth\) variables, that is, for \(\sigma\in [\pointersblock]\), the \(\sigma\)-th child contains the clause \(C \cup \{x^{\sigma_0}_{\alpha\noverdepth }, x^{\sigma_1}_{\alpha\noverdepth + 1}, \ldots,x^{\sigma_{\noverdepth-1}}_{\alpha\noverdepth + \noverdepth - 1}\}\) (recall that \(x_i^b = \neg x_i\) if \(b=0\) and \(x_i\) otherwise). Thus, \(\calT\) has \(2^n\) leaves, each containing a different clause of width \(n\).

6.4 The Reduction Function↩︎

We start by describing the decision trees that compute the variables of \(\myRef(F)\). For simplicity, we sometimes describe one decision tree that computes several variables at once.

6.4.0.1 Pointer variables.

The pointer variables of \(\eREF_d\) are defined in terms of the \(f\)-variables of \(\PHP(\expandergraph)\). Since each block has \(\pointersblock\) pointers, each layer \(\alpha\in \set{0, \dots, d-1}\) has a total of \(\blockslayer \cdot\pointersblock\) pointers that should be mapped to the \(\blockslayer\) blocks at level \(\alpha +1\). The idea is to define this mapping by “copying” the \(\PHP(\expandergraph)\) mapping from the \(\blockslayer\cdot\pointersblock\) pigeons to the \(\blockslayer\) holes. Formally, let \(B\) be an internal block, let \(z\in \zeroset{\pointersblock}\) and let \(i = \col(B) \cdot\pointersblock + z\). For all \(k\in [\delta]\), we define the pointer variables \(\point\bin^B_{z,k} = f_{i,k}\) and for all \(B'\) we define \(\point^B_{B',z} = 1\) if and only if \(\col(B') = \sur_i(f(i))\). This can clearly be done by a decision tree of depth \(\log \delta = O(n)\).

6.4.0.2 Enabled and literal variables.

We have now reached the most complicated part of the reduction. Consider the function \(g'\colon[\blockslayer]\to[\blockslayer\cdot\pointersblock]\cup \{\star\}\) defined as \[g'(j) = \left\{ \begin{array}{ll} g(j) & \text{ if } \sur_{g(j)}(f(g(j))) = j\,, \\ \star & \text{ otherwise.} \end{array}\right.\] In order to determine whether a block \(B\) is enabled or not and what literal set it contains, we recursively define a path of blocks and pointers starting from \(B\), denoted \(\pathB{B}\), in the following way. Let \(j=\col(B)\). If \(B\) is the root or if \(g'(j) = \star\), then the path ends at \(B\), that is, \(\pathB{B} = B\). Otherwise, let \[j' = \left\lfloor{\frac{g'(j)}{\blockslayer}}\right\rfloor \text{and} \sigma = g'(j) \mod \blockslayer \eqperiod\] Note that \(j'\) and \(\sigma\) are defined so that the \(\sigma\)th pointer of the block \(B'\) with \(\col(B') = j'\) and \(\layer(B') = \alpha - 1\) is \(j\). We define \(\pathB{B}\) to be \((B, \sigma)\) concatenated with \(\pathB{B'}\).

We are now ready to define a decision tree that computes the enabled variable and the literal variables of the block \(B\). In order to do so, the decision tree must compute \(\pathB{B}\), which can be done in depth \(O(\formuladepth (\log (\blockslayer \cdot \pointersblock) + \log \delta)) = O(n)\). Indeed, the length of \(\pathB{B}\) is at most \(\formuladepth\) and to determine the next block in a path it is enough to compute \(g'\), which can be done with \(O(\log (\blockslayer \cdot \pointersblock))=O(\noverdepth)\) queries to the \(g\)-variables and \(O(\log \delta) \le O(n/d)\) queries to the \(f\)-variables of \(\PHP(\expandergraph)\).

Once \(\pathB{B}\) is determined, the decision tree outputs the value of the variables as follows. If \(\pathB{B}\) does not end at the root, the enabled variable \(\enable^{B} = 0\), the literal variables \(\lit^{B}_{x_i} = 0\) for \(\ell \in \Lit\) (if B has \(\lit\) variables), and the summary variables \(\summlit_{i,z}^B\) are all set to \(1\). If \(\pathB{B}\) ends at the root, let \(\pi\) be the reverse of \(\pathB{B}\). Note that \(\pi\) defines a unique path in the tree \(\calT\) starting from the root and following the pointers in \(\pi\). This path in \(\calT\) ends in some block \(B'\) at level \(\alpha\). The decision tree sets the enabled variable \(\enable^{B}\) to \(1\) and sets the literal variables \(\lit^{B}_\ell\) for \(\ell \in \Lit\) to match the assignment of the block \(B'\).

6.4.0.3 Weakening variables.

The weakening variables are computed “honestly” given the assignments contained at the blocks at the last layer. That is, in order to determine the weakening variables for the block \(B\), the decision tree computes \(\pathB{B}\) (in depth \(O(n)\)), in this way determining the literal variables of \(B\), and then it outputs the value of each weakening variable \(\weak\) and \(\weak\bin\) so that this block points to an axiom \(A\) of \(F\) which it is the weakening of. Since there are \(n\) literals in \(B\) and \(F\) is unsatisfiable, such an \(A\) must exist. We note that, if \(\pathB{B}\) does not end at the root, then the literal variables and the enabled variable of \(B\) are all set to \(0\) and the weakening variables can point to an arbitrary axiom.

Therefore, we conclude that the reduction \(r\) satisfies the required condition that for each \(i\) there is a decision tree of depth \(O(n)\) that computes \(r_i\).

6.5 Correctness of the Reduction↩︎

We now show that the reduction satisfies the second condition of 5. Recall that \(\redfun\) is the function defined by the decision trees described above. Let \(D\) be an axiom of \(\myRef(F)\). It is enough to show that for every partial assignment \(\rho\) to the variables of \(\PHP(\expandergraph)\), if \(\rho\) falsifies \(D\circ r\) then \(\rho\) falsifies an axiom of \(\PHP(\expandergraph)\).

We first note that, by definition of \(\redfun\), if \(D\) is the root axiom [axiom:root-enabled]; a binary pointer axiom [axiom:point-binary-pointer]; a leaf axiom [axiom:must-appear-after-weak], [axiom:weaken-binary-pointer], or [axiom:summ-to-lits]; or a backchecking axiom [axiom:pass-on-summ-lits] or [axiom:pointer-to-summ-lits], then \(D\circ \redfun\) is a tautology, that is, for any full assignment \(\rho\) to the variables of \(\PHP(\expandergraph)\), the formula \(D\circ \redfun\) is satisfied.

It remains to consider the case when \(D\) is one of the [axiom:must-enable], [axiom:pass-on-summ-lits], or [axiom:pointer-to-summ-lits] axioms, that is \(( \enable^B \land \point^B_{B',z} ) \to \enable^{B'}\), \((\enable^B \land \point^B_{B',z'} \land \summlit_{i',z}^{B} ) \to \summlit_{i',z}^{B'}\) or \(( \enable^B \land \point^B_{B',z}) \to \summlit_{i+1,z}^{B'}\), respectively, for some \(B,B' \in [s]\) with \(i' \le i = \layer(B) = \layer(B') - 1\). In all three cases, for these clauses to be falsified, both \(\enable^B\) and \(\point^B_{B',z}\) must be set to \(1\). Note that \(\enable^B\) will only be set to \(1\) if \(\pathB{B}\) ends at the root and \(\point^B_{B',z}\) will only be set to \(1\) if \(\col(B') = \sur_j (f(j))\) for \(j = \col(B) \cdot 2^{\noverdepth} + z\).

Consider when \(D\) is one of the [axiom:must-enable] axioms. Note that \(\enable^{B'}\) will only be set to \(0\) in the reduction if \(\pathB{B'}\) does not end at the root. This implies that the value returned for \(g(\col(B'))\) was something other than \(j\) (corresponding to the \(z\)th pointer of \(B\)), since otherwise \(g'(\col(B'))\) would be equal to \(g(\col(B'))\) and \(\pathB{B'}\) would be \(\pathB{B}\) concatenated with \((B', B)\) and would, therefore, reach the root. Since \(\col(B') = \sur_j (f(j))\), the clause \(\sur_j (f(j)) = \col(B') \Rightarrow g(\col(B')) = j\) from \(\rPHP(G)\) is violated.

Now consider the case when \(D\) is one of the [axiom:pass-on-summ-lits] or [axiom:pointer-to-summ-lits] axioms. If the value returned for \(g(\col(B'))\) is \(j\) (corresponding to the \(z\)th pointer of \(B\)), then \(\pathB{B'}\) would go through \(B\) via the \(z\)th pointer of \(B\). This would imply that, in the case of [axiom:pass-on-summ-lits] both \(\summlit\) variables would be the same and thus [axiom:pass-on-summ-lits] would not be falsified; and in the case of [axiom:pointer-to-summ-lits] \(\summlit_{i+1,z}^{B'}\) would be \(1\), because \(\point^B_{B',z}\) is \(1\) and \(\layer(B) = i\), and thus [axiom:pointer-to-summ-lits] would not be falsified. So it must be the case that \(g(\col(B'))\) is not \(j\), and therefore we have that the clause \(\sur_{j} (f(j)) = \col(B') \Rightarrow g(\col(B')) = j\) from \(\rPHP(G)\) is violated.

References↩︎