Can every \(n\)-bit boolean function with deterministic query complexity \(k\ll n\) be restricted to \(O(k)\) variables such that the query complexity remains \(\Omega(k)\)? That is, can query complexity be condensed via restriction? We study such hardness condensation questions in both query and communication complexity, proving two main results.
- Negative: Query complexity cannot be condensed in general: There is a function \(f\) with query complexity \(k\) such that any restriction of \(f\) to \(O(k)\) variables has query complexity \(O(k^{3/4})\).
- Positive: Randomised communication complexity can be condensed for the sink-of-xor function. This yields a quantitatively improved counterexample to the log-approximate-rank conjecture, achieving parameters conjectured by [Chattopadhyay, Garg, and Sherif, 2021].
Along the way we show the existence of
Shearer extractors --- a new type of seeded extractor whose output bits satisfy prescribed dependencies across distinct seeds.
A hitting formula is a set of Boolean clauses such that any two of the clauses cannot be simultaneously falsified. Hitting formulas have been studied in many different contexts at least since
[Iwama, 1989] and, based on experimental evidence,
[Peitl and Szeider, 2022] conjectured that unsatisfiable hitting formulas are among the hardest for resolution.Using the fact that hitting formulas are easy to check for satisfiability we make them the foundation of a new static proof system Hitting: a refutation of a CNF in Hitting is an unsatisfiable hitting formula such that each of its clauses is a weakening of a clause of the refuted CNF. Comparing this system to resolution and other proof systems is equivalent to studying the hardness of hitting formulas. Our first result is that Hitting is quasi-polynomially simulated by tree-like resolution, which means that hitting formulas cannot be exponentially hard for resolution and partially refutes the conjecture of Peitl and Szeider. We show that tree-like resolution and Hitting are quasi-polynomially separated, while for resolution, this question remains open. For a system that is only quasi-polynomially stronger than tree-like resolution, Hitting is surprisingly difficult to
polynomially simulate in another proof system. Using the ideas of Raz-Shpilka's polynomial identity testing for noncommutative circuits
[Raz, Shpilka, 2005] we show that Hitting is p-simulated by Extended Frege, but we conjecture that much more efficient simulations exist. As a byproduct, we show that a number of static (semi)algebraic systems are verifiable in deterministic polynomial time.
We present a top-down lower-bound method for depth-\(4\) boolean circuits. In particular, we give a new proof of the well-known result that the parity function requires depth-\(4\) circuits of size exponential in \(n^{1/3}\). Our proof is an application of robust sunflowers and block unpredictability.
A circuit \(\mathcal{C}\) samples a distribution X with an error \(\epsilon\) if the statistical distance between the output of \(\mathcal{C}\) on the uniform input and X is \(\epsilon\). We study the hardness of sampling a uniform distribution over the set of \(n\)-bit strings of Hamming weight \(k\) denoted by \(\mathbf{U}^n_k\) for decision forests, i.e. every output bit is computed as a decision tree of the inputs. For every \(k\) there is an \(O(\log n)\)-depth decision forest sampling \(\mathbf{U}^n_k\) with an inverse-polynomial error [Viola 2012], [Czumaj 2015]. We show that for every \(\epsilon > 0\) there exists \(\tau\) such that for decision depth \(\tau \log (n/k) / \log \log (n/k)\), the error for sampling \(\mathbf{U}^n_k\) is at least \(1-\epsilon\). Our result is based on the recent robust sunflower lemma [Alweiss, Lovett, Wu, Zhang 2019], [Rao 2019].
Our second result is about matching a set of \(n\)-bit strings with the image of a \(d\)-local circuit, i.e. such that each output bit depends on at most \(d\) input bits. We study the set of all \(n\)-bit strings whose Hamming weight is at least \(n/2\). We improve the previously known locality lower bound from \(\Omega(\log^* n)\) [BDKMSSTV 2013] to \(\Omega(\sqrt{\log n})\), leaving only a quartic gap from the best upper bound of \(O(\log^2 n)\).
A subcube partition is a partition of the Boolean cube \(\{0,1\}^n\) into subcubes. A subcube partition is irreducible if the only sub-partitions whose union is a subcube are singletons and the entire partition. A subcube partition is tight if it “mentions” all coordinates.
We study extremal properties of tight irreducible subcube partitions: minimal size, minimal weight, maximal number of points, maximal size, and maximal minimum dimension. We also consider the existence of homogeneous tight irreducible subcube partitions, in which all subcubes have the same dimensions. We additionally study subcube partitions of \(\{0,1,\dots,q-1\}^n\), and partitions of \(\mathbb{F}_2^n\) into affine subspaces, in both cases focusing on the minimal size.
Our constructions and computer experiments lead to several conjectures on the extremal values of the aforementioned properties.
We show that every read-once nondeterministic branching program computing the Minimum Circuit Size Problem on inputs of length \(N\) has size \(\Omega(N^{\log\log(N)})\). This is the first superpolynomial lower bound on the size of a read-once branching program computing MCSP. This lower bound is tight for the version of MCSP restricted to a linear circuit size parameter.
To show this result we adapt a conditional lower bound of [Ilango, 2020] on the deterministic Turing Machine time complexity of computing \(\mathrm{MCSP}^{*}\), the generalization of MCSP to partial functions. In contrast, our lower bound is unconditional and holds even for the total MCSP function.
We prove that the proof system \(\mathrm{OBDD}(\land, \mathrm{weakening})\) is not automatable unless P=NP. The proof is based upon the celebrated result of
[Atserias, Muller 2019] about the hardness of automatability for resolution. The heart of the proof is lifting with multi-output indexing gadget from resolution block-width to dag-like multiparty number-in-hand communication protocol size with \(o(n)\) parties, where \(n\) is the number of variables in the non-lifted formula. A similar lifting theorem for protocols with \(n+1\) participants was proved by
[Göös, Koroth, Mertz, Pitassi, 2020] to establish the hardness of automatability result for Cutting Planes.
We show that for any connected graph \(G\) the size of any regular resolution or \(\mathrm{OBDD}(\land, \mathrm{reordering})\) refutation of a Tseitin formula based on \(G\) is at least \(2^{\Omega(\mathrm{tw}(G))}\), where \(\mathrm{tw}(G)\) is the treewidth of \(G\). These lower bounds improve upon the previously known bounds and, moreover, they are tight.
We prove that the size of any regular resolution refutation of a Tseitin formula \(\mathrm{Ts}(G,c)\) based on a connected graph \(G=(V,E)\) is at least \(2^{\Omega(\mathrm{tw}(G)/\log |V|)}\), where \(\mathrm{tw}(G)\) denotes the treewidth of a graph \(G\). For constant-degree graphs there is known upper bound \(2^{O(\mathrm{tw}(G))}\mathrm{poly}(|V|)\)
[Alekhnovich, Razborov, 2011],
[Galesi, Talebanfard, Torán 2020], so our lower bound is tight up to a logarithmic factor in the exponent.
We show two communication lower bounds on the clause search problem \(\mathrm{Search}_\phi\), the problem is given an assignment to the variables of an unsatisfiable CNF \(\phi\) find a clause \(C \in \phi\) that is falsified by the assignment. The first lower bound is on the 2-party communication cost of \(\mathrm{Search}_\phi\) with \(\phi\) encoding the perfect matching principle over the graph \(K_{n,n+2}\), the second is a on the number-on-forehead communication complexity of \(\mathrm{Search}_\phi\) where \(\phi\) is the bitwise encoding of the pigeonhole principle. These communication lower bounds imply several interesting proof complexity lower bounds that seemed unattainable via communication reductions.
This paper is motivated by seeking lower bounds on \(\mathrm{OBDD}(\land, \mathrm{weakening}, \mathrm{reordering})\) refutations, namely OBDD refutations that allow weakening and arbitrary reorderings. We first work with \(1\text{-}\mathrm{NBP}(\land)\) refutations based on read-once nondeterministic branching programs. These generalize \(\mathrm{OBDD}(\land, \mathrm{reordering})\) refutations. There are polynomial size \(1\text{-}\mathrm{NBP}(\land)\) refutations of the pigeonhole principle, hence \(1\text{-}\mathrm{NBP}(\land)\) is strictly stronger than \(\mathrm{OBDD}(\land, \mathrm{reordering})\). There are also formulas that have polynomial size tree-like resolution refutations but require exponential size \(1\text{-}\mathrm{NBP}(\land)\) refutations. As a corollary, \(\mathrm{OBDD}(\land, \mathrm{reordering})\)does not simulate tree-like resolution, answering a previously open question.
The system \(1\text{-}\mathrm{NBP}(\land, \exists)\) uses projection inferences instead of weakening. \(1\text{-}\mathrm{NBP}(\land, \exists_k)\) is the system restricted to projection on at most \(k\) distinct variables. We construct explicit constant degree graphs \(G_n\) on \(n\) vertices and an \(\epsilon > 0\), such that \(1\text{-}\mathrm{NBP}(\land, \exists_{\epsilon n})\) refutations of the Tseitin formula for \(G_n\) require exponential size.
Second, we study the proof system \(\mathrm{OBDD}(\land, \mathrm{weakening}, \mathrm{reordering}_\ell)\) which allows \(\ell\) different variable orders in a refutation. We prove an exponential lower bound on the complexity of tree-like \(\mathrm{OBDD}(\land, \mathrm{weakening}, \mathrm{reordering}_\ell)\) refutations for \(\ell = \epsilon \log n\), where \(n\) is the number of variables and \(\epsilon > 0\) is a constant. The lower bound is based on multiparty communication complexity.
We prove that there is a constant \(K\) such that
Tseitin formulas for an undirected graph \(G\) requires proofs of size \(2^{\mathrm{tw}(G)^{\Omega(1/d)}}\) in depth \(d\) Frege systems for \(d<\frac{K \log n}{\log \log n}\), where \(\mathrm{tw}(G)\) is the treewidth of \(G\). This extends Hastad's recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent. Namely, we show that if a Tseitin formula for a graph \(G\) has size \(s\), then for all large enough \(d\), it has a depth \(d\) Frege proof of size \(2^{\mathrm{tw}(G)^{O(1/d)}} \mathrm{poly}(s)\). Through this result we settle a question posed by
[Alekhnovich, Razborov, 2011] about the efficient search for resolution proofs of Tseitin formulas over any graph.
We introduce a propositional proof system based on decision trees utilizing symmetries of formulas. We refer to this proof system as decision trees with symmetries (SDT). SDT can be polynomially simulated by the proof system SR-I introduced by
[Krishnamurthy, 1985]; SR-I extends Resolution with the symmetry rule. We show that there are polynomial-size proofs of the functional pigeonhole principle \(\mathrm{FPHP}_n^{n+1}\) and of an encoding of the clique coloring principle. On the other hand we show that any SDT for the pigeonhole principle \(\mathrm{PHP}_n^{n+1}\) has size \(2^{n^{1/3-o(1)}}\) despite that the pigeonhole principle has a lot of symmetries.
