Conditional Complexity Hardness: Monotone Circuit Size, Matrix Rigidity, and Tensor Rank

As unconditional complexity lower bounds remain elusive, the classical complexity theory allows one to prove conditional lower bounds of the following form: if a problem $A$ cannot be solved in polynomial-time, then $B$ also cannot be solved in polynomial-time. Such results are proved via reductions that are essentially algorithms: one shows how to transform an instance of $A$ into an instance of $B$. Nowadays, hundreds of such reductions between various $\mathrm{𝖭𝖯}$-hard problems are known. For instance, if $\mathrm{𝖲𝖠𝖳}$ cannot be solved in polynomial-time, then the Hamiltonian Cycle problem also cannot be solved in polynomial-time.

In a recently emerged area of fine-grained complexity, one aims to construct tighter reductions between problems showing that even a tiny improvement of an algorithm for one of them automatically leads to improved algorithms for the other one. For example, as proved by Williams [100], if $\mathrm{𝖲𝖠𝖳}$ cannot be solved in time $O(2^{(1-\epsilon )n})$, for any $\epsilon >0$, then the Orthogonal Vectors problem cannot be solved in time $O(n^{2-\epsilon })$, for any $\epsilon >0$. Again, many reductions of this form have been developed in recent years. We refer the reader to a recent survey by Vassilevska Williams [97].

One of the reasons why proving complexity lower bounds is challenging is that an algorithm (viewed as a Turing machine or a RAM machine) is a relatively complex object: it has a memory, may contain loops, function calls (that may in turn be recursive). A related computational model of Boolean circuits has a much simpler structure (a straight-line program) and at the same time is powerful enough to model algorithms: if a problem can be solved by algorithms in time $T(n)$, then it can also be solved by circuits of size $O(T(n)\log T(n))$ [76]. It turns out that proving circuit lower bounds is also challenging: while it is not difficult to show that almost all Boolean functions can be computed by circuits of exponential size only (this was proved by Shannon [88] back in 1949), for no function from $\mathrm{𝖭𝖯}$, we can currently exclude the possibility that it can be computed by circuits of linear size [66, 34]. Strong lower bounds are only known for restricted models such as monotone circuits, constant-depth circuits, and formulas. Various such unconditional lower bounds can be found in the book by Jukna [61].

An important difference between algorithms and circuits is that algorithms represent a uniform model of computation (an algorithm is a program that needs to process instances of all possible lengths), whereas circuits are nonuniform: when saying that a problem can be solved by circuits, one usually means that there is an infinite collection of circuits, one circuit for every possible input length, and different circuits in this collection can, in principle, implement different programs. This makes the circuit model strictly more powerful than algorithms: on the one hand, every problem solved by algorithms can be solved by circuits of roughly the same size; on the other hand, it is not difficult to come up with a problem of small circuit size that cannot be solved by algorithms.

Intuitively, it seems that proving complexity upper bounds should be easier than proving lower bounds. This intuition is well supported by a much higher number of results on algorithms compared to the number of results on lower bounds. Indeed, to prove an upper bound on the complexity of a problem, one designs an algorithm for the problem and analyzes it. Whereas to prove a complexity lower bound, one needs to reason about a wide range of fast algorithms (or small circuits) and to argue that none of them is able to solve the problem at hand. Perhaps surprisingly, the tasks of proving lower and upper complexity bounds are connected to each other. A classical example is Karp–Lipton theorem [62] stating that if $𝖯$ = $\mathrm{𝖭𝖯}$, then $\mathrm{𝖤𝖷𝖯}$ requires circuits of size $\mathrm{\Omega }(2^n/n)$. More recently, Williams [102] established a deep connection between an upper bound for Circuit SAT and circuit lower bounds. Extending his results, Jahanjou, Miles and Viola [59] proved that if $\mathrm{𝖭𝖲𝖤𝖳𝖧}$ is false (meaning that $\mathrm{𝖴𝖭𝖲𝖠𝖳}$ can be solved fast with nondeterminism), then $𝖤{}^{\mathrm{𝖭𝖯}}$ requires series-parallel Boolean circuits of size $\omega (n)$. Such results show how to derive nonuniform lower bounds (that is, circuit lower bounds) from uniform upper bounds (algorithm upper bounds).

Even though one can simulate an algorithm using circuits with slight overhead, the converse is not true as there are undecidable languages of low circuit complexity. Recently, [12] showed results analogous to those presented herein, particularly on deriving a nonuniform lower bound from a non-randomized uniform lower bound. Specifically, they proved that if $\mathrm{𝖬𝖠𝖷}$-$k$-$\mathrm{𝖲𝖠𝖳}$ cannot be solved in co-nondeterministic time $O(2^{(1-\epsilon )n})$, for any $\epsilon >0$, then, for any $\delta >0$, there exists an explicit polynomial family that cannot be computed by arithmetic circuits of size $O(n^{\delta })$. Also, Williams [103] proved that if the Orthogonal Vectors conjecture ($\mathrm{𝖮𝖵𝖢}$) holds, then Boolean Inner Product on $n$-bit vectors cannot be computed by $\mathrm{𝖤𝖳𝖧𝖱}\circ \mathrm{𝖤𝖳𝖧𝖱}$ circuits of size $2^{\epsilon n}$, for some $\epsilon >0$. Combined with the result above (since $\mathrm{𝖮𝖵𝖢}$ is weaker than $\mathrm{𝖭𝖲𝖤𝖳𝖧}$), it immediately leads to win-win circuit lower bounds: if $\mathrm{𝖭𝖲𝖤𝖳𝖧}$ fails, we have a lower bound for series-parallel circuits, otherwise we have a strong lower bound for $\mathrm{𝖤𝖳𝖧𝖱}\circ \mathrm{𝖤𝖳𝖧𝖱}$ circuits.

In this paper, we derive a number of nonuniform lower bounds from uniform nondeterministic lower bounds. Our lower bounds apply to various objects that are notoriously hard to analyze: Boolean functions of high monotone circuit size, high rigidity matrices, and high rank tensors. For circuits, we get a win-win situation similar to the one by Williams.

Our first result shows how to get $2^{\mathrm{\Omega }(n/\log n)}$ monotone circuit lower bounds (improving best known bounds of the form $2^{\mathrm{\Omega }(\sqrt{n})}$) under an assumption that $\mathrm{𝖲𝖠𝖳}$ requires co-nondeterministic time $O(2^{(1/2+\epsilon )n})$ if the verifier is given a proof that depends only on the length of the input.

As the previous theorem uses a weaker assumption than $\mathrm{𝖭𝖲𝖤𝖳𝖧}$, we get the following corollary.

Combining this with circuit lower bounds that follow from the negation of $\mathrm{𝖭𝖲𝖤𝖳𝖧}$ due to [59, 22] (see Theorem 11), leads to win-win circuit lower bounds.

Each of these lower bounds is far from what is currently known: the best known circuit lower bound for ${𝖤}^{\mathrm{𝖭𝖯}}$ is $3.1n-o(n)$ [66], whereas the best known monotone circuit lower bound for $\mathrm{𝖼𝗈𝖭𝖯}$ is $2^{\mathrm{\Omega }(\sqrt{n})}$ (see Section 1.2).

Another result in this direction demonstrates how to derive circuit lower bounds from $\mathrm{𝖭𝖤𝖳𝖧}$ (which asserts that $3$-$\mathrm{𝖲𝖠𝖳}$ cannot be solved in co-nondeterministic time $2^{o(n)}$). Specifically, we establish lower bounds for the classes $Q_t^n$.

These sets have been studied in secure multiparty computation [54, 35, 55] and from a complexity-theoretic perspective [29, 64]. It turns out that the class $Q_t^n$ coincides precisely with the set of functions $f$ for which there exists a circuit $C$, composed solely of ${\mathrm{𝖳𝖧𝖱}}_{l+1}^{lt+1}$ gates for arbitrary $l\ge 1$, such that $C\le f$ [29, 64]¹¹1By $C\le f$, we mean that $C(x)\le f(x)$ for all inputs $x$..

Our result indicates that $Q_t^n$ contains functions that are exponentially hard to represent using ${\mathrm{𝖳𝖧𝖱}}_{l+1}^{lt+1}$ gates only while being easy to compute by regular circuits.

Our second result shows how to construct small families of matrices with rigidity exceeding the best known constructions under an assumption that $\mathrm{𝖬𝖠𝖷}$-3-$\mathrm{𝖲𝖠𝖳}$ requires co-nondeterministic time nearly $2^n$.

Our third result extends the second result by including high-rank tensors.

It is worth noting that [12] showed circuit lower bounds under the same assumption: if $\mathrm{𝖬𝖠𝖷}$-$k$-$\mathrm{𝖲𝖠𝖳}$ cannot be solved in co-nondeterministic time $O(2^{(1-\epsilon )n})$ for any $\epsilon >0$, then for any $\delta >0$, there exists an explicit polynomial family that cannot be computed by arithmetic circuits of size $O(n^{\delta })$.

The best known lower bound for the size of depth-three circuits computing an explicit Boolean function is $2^{\mathrm{\Omega }(\sqrt{n})}$ [51, 75]. Proving a $2^{\omega (\sqrt{n})}$ lower bound for this restricted circuit model remains a challenging open problem and it is known that a lower bound as strong as $2^{\omega (n/\log \log n)}$ would give an $\omega (n)$ lower bound for unrestricted circuits via Valiant’s reduction [96]. One way of proving better depth-three circuit lower bounds is via canonical circuits introduced by Goldreich and Wigderson [42]. They are closely related to rigid matrices: if $T$ is an $n\times n$ matrix of $r$-rigidity $r^3$, then the corresponding bilinear function requires canonical circuits of size $2^{\mathrm{\Omega }(r)}$ [42]. Goldreich and Tal [41] showed that a random Toeplitz matrix has $r$-rigidity $\frac{n^3}{r^2\log n}$, which implies a $2^{\mathrm{\Omega }(n^{3/5})}$ lower bound on canonical depth-three circuits for an explicit function. By substituting $n^{2/3-\delta }$-rigidity for some $\delta >0$ in Theorem 7, one gets the following result.

This conditionally improves the recent result of Goldreich [40], who presented an $O(1)$-linear function that requires canonical depth-two circuits of size $2^{\mathrm{\Omega }(n^{1-\epsilon })}$, for every $\epsilon >0$. Moreover, every bilinear function can be computed by canonical circuits of size $2^{O(n^{2/3})}$, so the lower bound is almost optimal and conditionally addresses Open Problem 6.5 from [41].

In this section, we review known constructions of combinatorial objects (functions of high monotone circuit size, matrices of high rigidity, and tensors of high rank).

Many of the lower bounds mentioned above are proved under various strong assumptions (on the complexity of $\mathrm{𝖲𝖠𝖳}$, $\mathrm{𝖬𝖠𝖷}$-$\mathrm{𝖲𝖠𝖳}$, Set Cover, Chromatic Number, Traveling Salesman). They seem much stronger than merely $𝖯\ne \mathrm{𝖭𝖯}$ and might eventually be refuted. Still, the revealed reductions between problems are of great interest and may still yield further insights: one may be able to weaken the used assumptions or to construct generators from other fine-grained reductions. Moreover, as with the case of $\mathrm{𝖭𝖲𝖤𝖳𝖧}$ assumption, one may be able to derive interesting consequences from both an assumption and its negation leading to a win-win situation. Below, we state a few open problems in this direction.

If one were to partition $3$-$\mathrm{𝖲𝖠𝖳}$ in Theorem 12 into $t$ parts, where $t=\omega (1)$, then creating an explicit function equivalent to $t$-$\mathrm{𝖮𝖵}$ would imply lower bounds for that function under $\mathrm{𝖭𝖤𝖳𝖧}$. This approach would yield a more advantageous win-win situation, as the assumption that $\mathrm{𝖭𝖤𝖳𝖧}$ is false gives stronger lower bounds [27].

Moreover, the existence of small monotone circuits not only refutes $\mathrm{𝖭𝖲𝖤𝖳𝖧}$ but also establishes that $\mathrm{𝖴𝖭𝖲𝖠𝖳}$ has input-oblivious proof size $2^{o(n)}$ that can be verified in time $2^{\frac{n}{2}+o(n)}$. Therefore, we believe that it may be possible to derive even stronger implications beyond merely refuting $\mathrm{𝖭𝖲𝖤𝖳𝖧}$.

Another question arises regarding tensor rank. Is it possible to construct a small family of tensors with superlinear rank, assuming that $\mathrm{𝖬𝖠𝖷}$-3-$\mathrm{𝖲𝖠𝖳}$ cannot be solved efficiently in co-nondeterministic time (this way, eliminating the dependence on rigidity from our results)?

However, we do not know of any consequences of solving $\mathrm{𝖬𝖠𝖷}$-3-$\mathrm{𝖲𝖠𝖳}$ faster in the co-nondeterministic setting. This makes our assumption weak and raises the question of whether it can be refuted.

On the other hand, to get a win-win situation, it would be interesting to find nontrivial consequences of the existence of such an algorithm.

The paper is organized as follows. In Section 2, we give an overview of the main proof ideas. In Section 3, we introduce the notation used throughout the paper and provide the necessary background. In Section 4, we establish the win-win circuit lower bound. In Section 5, we construct rigid matrices under an assumption that $\mathrm{𝖬𝖠𝖷}$-3-$\mathrm{𝖲𝖠𝖳}$ cannot be solved fast co-nondeterministically. In Section 6, we construct either three-dimensional tensors with high rank or matrices with high rigidity under the same assumption. The proofs of certain statements are omitted due to the page limit. They can be found in the full version [28].

To prove a lower bound $2^{\mathrm{\Omega }(n/\log n)}$ for monotone circuit size of $\mathrm{𝖼𝗈𝖭𝖯}$ under $\mathrm{𝖭𝖲𝖤𝖳𝖧}$, we assume that all monotone functions from $\mathrm{𝖼𝗈𝖭𝖯}$ have monotone circuit size $2^{o(n/\log n)}$ and show how this can be used to solve $\mathrm{𝖴𝖭𝖲𝖠𝖳}$ nondeterministically in less than $2^n$ steps.

Given a $k$-CNF $F$, we construct an instance $(A_F,B_F)$ of $\mathrm{𝖮𝖵}$ of size $2^{n/2}$ using Theorem 12. We show (see Lemma 15) that $(A_F,B_F)$ is a yes-instance if and only if there exists a monotone Boolean function separating $(A_F,\overline{B_F})$. Hence, one can guess a small monotone circuit separating $(A_F,\overline{B_F})$ and verify that it is correct. Overall, the resulting nondeterministic algorithm proceeds as follows.

1. 1.

   In time $O(n^2{2}^{n/2})$, generate the sets $A_F$ and $B_F$.

2. 2.

   Guess a monotone circuit $C_F$ of size $O(2^{(1-\epsilon )n/2})$.

3. 3.

   Verify that $C_F$ separates $(A_F,\overline{B_F})$. To do this, check that $C_F(a)=1$, for every $a\in A_F$. Then, check that $C_F(b)=0$, for every $b\in \overline{B_F}$. The running time of this step is

   $$O(2^{(1-\epsilon )n/2}\cdot |A_F|+2^{(1-\epsilon )n/2}\cdot |\overline{B_F}|)=O(2^{(1-\epsilon )n/2}\cdot 2^{n/2})=O(2^{(1-\epsilon /2)n}).$$

4. 4.

   If $C_F$ separates $(A_F,\overline{B_F})$, then $F\in \mathrm{𝖴𝖭𝖲𝖠𝖳}$.

This already shows how small monotone circuits could help to break $\mathrm{𝖭𝖲𝖤𝖳𝖧}$, though it does not provide a single explicit function with this property. In the full proof in Section 4, we introduce such a function. We also use a weaker assumption (than $\mathrm{𝖭𝖲𝖤𝖳𝖧}$).

To construct matrices of high rigidity under the assumption that $\mathrm{𝖬𝖠𝖷}$-$3$-$\mathrm{𝖲𝖠𝖳}$ cannot be solved fast co-nondeterministically, we proceed as follows. Take a $3$-CNF formula over $n$ variables and an integer $t$ and transform it, using Theorem 14, into a $4$-partite $3$-uniform hypergraph $G$ with each part of size $k=n^{O(1)}{2}^{\frac{n}{4}}$. The graph $G$ contains a $4$-clique if and only if one can satisfy $t$ clauses of $F$. We show that checking whether $G$ has a $4$-clique is equivalent to evaluating a certain expression over three-dimensional tensors. We then show that if all slices of these tensors have low rigidity, then one can solve $4$-Clique on $G$ in co-nondeterministic time $O(k^{4-\epsilon })$: to achieve this, one guesses a decomposition of a matrix into a sum of a low rank matrix and a matrix with few nonzero entries. The idea is that a low rank matrix can be guessed quickly as a decomposition into rank-one matrices (which are just products of two vectors), whereas the second matrix can be guessed quickly as one needs to guess the nonzero entries only. In turn, this allows one to solve $\mathrm{𝖬𝖠𝖷}$-$3$-$\mathrm{𝖲𝖠𝖳}$ faster than $2^n$ co-nondeterministically. Thus, this reduction is a generator of rigid matrices: it takes a $3$-CNF formula and outputs a matrix. The same idea can be used to generate either tensors with high rank or matrices with high rigidity.

For a CNF formula $F$, by $n(F)$ and $m(F)$ we denote the number of variables and clauses of $F$, respectively. We write just $n$ and $m$, if the corresponding CNF formula is clear from the context. In $\mathrm{𝖲𝖠𝖳}$ ($\mathrm{𝖴𝖭𝖲𝖠𝖳}$), one is given a CNF formula and the goal is to check whether it is satisfiable (unsatisfiable, respectively). In $k$-$\mathrm{𝖲𝖠𝖳}$, the given formula is in $k$-CNF (that is, all clauses have at most $k$ literals). In $\mathrm{𝖬𝖠𝖷}$-$k$-$\mathrm{𝖲𝖠𝖳}$, one is given a $k$-CNF and an integer $t$ and is asked to check whether it is possible to satisfy exactly $t$ clauses.

When designing an algorithm for $\mathrm{𝖲𝖠𝖳}$, one can assume that the input formula has a linear (in the number of variables) number of clauses. This is ensured by the following Sparsification Lemma. By $(\beta ,k)$-$\mathrm{𝖲𝖠𝖳}$, we denote a special case of $k$-$\mathrm{𝖲𝖠𝖳}$ where the input $k$-CNF formula has at most $\beta n$ clauses.

The proof of Corollary 10 can be found in the full version [28].

The Strong Exponential Time Hypothesis ($\mathrm{𝖲𝖤𝖳𝖧}$), introduced in [58, 57], asserts that, for any $\epsilon >0$, there is $k$ such that $k$-$\mathrm{𝖲𝖠𝖳}$ cannot be solved in time $O(2^{(1-\epsilon )n})$. The Nondeterministic $\mathrm{𝖲𝖤𝖳𝖧}$ ($\mathrm{𝖭𝖲𝖤𝖳𝖧}$), introduced in [22], extends $\mathrm{𝖲𝖤𝖳𝖧}$ by asserting that $\mathrm{𝖲𝖠𝖳}$ is difficult even for co-nondeterministic algorithms: for any $\epsilon >0$, there is $k$ such that $k$-$\mathrm{𝖲𝖠𝖳}$ cannot be solved in co-nondeterministic time $O(2^{(1-\epsilon )n})$. Though both these statements are stronger than $𝖯\ne \mathrm{𝖭𝖯}$, they are known to be hard to refute: as proved by Jahanjou, Miles and Viola [59], if $\mathrm{𝖲𝖤𝖳𝖧}$ is false, then there exists a Boolean function family in ${𝖤}^{\mathrm{𝖭𝖯}}$ of series-parallel circuit size $\omega (n)$. [22] noted that it suffices to refute $\mathrm{𝖭𝖲𝖤𝖳𝖧}$ to get the same circuit lower bound.

$\mathrm{𝖲𝖤𝖳𝖧}$-based conditional lower bounds are known for a wide range of problems and input parameters. One of such problems is Orthogonal Vectors ($\mathrm{𝖮𝖵}$): given two sets $A,B\subseteq {\{0,1\}}^d$ of size $n$, check whether there exists $a\in A$ and $b\in B$ such that $a\cdot b={\sum }_{i\in [d]}{a}_i{b}_i=0$. It is straightforward to see that $\mathrm{𝖮𝖵}$ can be solved in time $O(n^{2}d)$. Williams [100] proved that under $\mathrm{𝖲𝖤𝖳𝖧}$, there is no algorithm solving $\mathrm{𝖮𝖵}$ in time $O(n^{2-\epsilon }{d}^{O(1)})$, for any $\epsilon >0$. This follows from the following reduction.

In a similar manner, one can reduce a CNF formula to the $t$-$\mathrm{𝖮𝖵}$ problem involving a greater number of sets. Consider the $t$-$\mathrm{𝖮𝖵}$ problem, where one is given $t$ sets $A^1,\mathrm{\dots },A^t\subseteq {\{0,1\}}^d$, each of size $n$, and the objective is to determine whether there exist elements $a^1\in A^1,\mathrm{\dots },a^t\in A^t$ such that ${\sum }_{i\in [d]}{a}_i^1\cdot \mathrm{\dots }\cdot a_i^t=0$.

The proof follows the approach presented in [100]. An instance $(A^1,\mathrm{\dots },A^t)\notin t$-$\mathrm{𝖮𝖵}$ if and only if for all vectors $a^1\in A^1,\mathrm{\dots },a^t\in A^t$, the vectors share a common coordinate with value one. This can equivalently be formulated by stating that the union $Q=A^1\cup \mathrm{\dots }\cup A^t$ possesses the property that for every $a^1,\mathrm{\dots },a^t\in Q$, the vectors share a common one. Consequently, the instance $(A^1,\mathrm{\dots },A^t)\notin t$-$\mathrm{𝖮𝖵}$ if and only if there exists a circuit $C$, composed of ${\mathrm{𝖳𝖧𝖱}}_{l+1}^{lt+1}$ gates and variables, such that $C(\overline{x})=0$ for every $x\in A^1\cup \mathrm{\dots }\cup A^t$.

A similar reduction allows to solve $\mathrm{𝖬𝖠𝖷}$-3-$\mathrm{𝖲𝖠𝖳}$ by finding a $4$-clique in a $3$-uniform hypergraph. A subset of $l$ nodes in a $k$-hypergraph is called an $l$-clique, if any $k$ of them form an edge in the graph.

The proof is given in the full version [28].

For a field $𝔽$, by ${𝔽}^{a\times b}$ we denote the set of all matrices of size $a\times b$ over $𝔽$. Similarly, by ${𝔽}^{a\times b\times c}$ we denote the set of all three-dimensional tensors of shape $a\times b\times c$ over $𝔽$. For two tensors $A$ and $B$ (of arbitrary shape), by $A\otimes B$ we denote a tensor product of $A$ and $B$. For a matrix $M\in {𝔽}^{a\times b}$, by $|M|$ we denote the number of nonzero entries of $M$.

For a matrix $M\in {𝔽}^{a\times b}$, we say that it has $r$-rigidity $s$ if it is necessary to change at least $s$ entries of $M$ to reduce its rank to $r$. That is, for each decomposition $M=R+S$ such that $\mathrm{rank}(R)\le r$, it holds that $|S|\ge s$.

The rank of a three-dimensional tensor is a natural extension of the matrix rank. For a tensor $𝒜\in {𝔽}^{n\times n\times n}$, we define its rank, $\mathrm{rank}(𝒜)$, as the smallest integer $r$ such that there exist $r$ tuples of vectors $a_l,b_l,c_l\in {𝔽}^n$ for which

or equivalently,

for all $i,j,k\in [n]$.

We denote by $\omega$ the smallest real number such that any two $n\times n$ matrices can be multiplied in time $O(n^{\omega +\epsilon })$ for any $\epsilon >0$ using only field operations³³3The value of $\omega$ may depend on the field over which the calculations are performed [87]..

Consider the three-dimensional tensor ${𝒜}_n\in {𝔽}^{n^2\times n^2\times n^2}$:

for all $i,j,k\in [n]$, with all other entries being zero. Using an approach based on the work of Strassen [92], for any positive integer $k$, if $\mathrm{rank}({𝒜}_k)=q$, then one can construct an arithmetic circuit of size $O(n^{{\log }_k(q)})$ to perform multiplication of two $n\times n$ matrices. Thus, $\omega$ satisfies the following equation:

In other words, for sufficiently large $k$, we have that $\mathrm{rank}({𝒜}_k)\ge k^{\omega }$. Specifically, if $n=k^2$, then ${𝒜}_k\in {𝔽}^{n\times n\times n}$, and $\mathrm{rank}({𝒜}_k)\ge n^{\omega /2}$. Therefore, if $\omega >2$, this yields superlinear lower bounds on arithmetic circuits and on the rank of the multiplication tensor.

The best known upper bound on $\omega$ is $2.371339$ [98, 3]. Further details on the matrix multiplication tensor can be found in [5, 19].

In this section, we prove Theorem 1.

Combining this with Corollary 2 and Theorem 11, we get win-win circuit lower bounds. Proving any of these two circuit lower bounds is a challenging open problem.

For the proof of Theorem 1, we need two technical lemmas. Recall that the reduction from $\mathrm{𝖲𝖠𝖳}$ to $\mathrm{𝖮𝖵}$ (see Theorem 12), given a formula $F$, produces two sets $A_F,B_F\subseteq {\{0,1\}}^{m(F)}$ such that $|A_F|=|B_F|=2^{n(F)/2}$ and $F\in \mathrm{𝖲𝖠𝖳}$ if and only if $(A_F,B_F)\in \mathrm{𝖮𝖵}$.

For a CNF formula $F$, let $f_F:{\{0,1\}}^{m(F)}\to \{0,1\}$ be defined as follows:

It is immediate that $f_F$ is monotone and that $\overline{B_F}\subseteq f_F^{-1}(0)$.