We prove superpolynomial length lower bounds for the semantic tree-like Frege refutation system with bounded line size. Concretely, for any function $n^{2-\varepsilon} \leq s(n) \leq \exp\bigl(n^{1-\varepsilon}\bigr)$ we exhibit an explicit family $\mathcal{A}$ of $n$-variate CNF formulas $A$, each of size $|A| \le s(n)^{1+\varepsilon}$, such that if $A$ is chosen uniformly ... more >>>

The seminal work of Benczu}r and Karger demonstrated cut sparsifiers of near-linear size, with several applications throughout theoretical computer science. Subsequent extensions have yielded sparsifiers for hypergraph cuts and more recently linear codes over Abelian groups. A decade ago, Kogan and Krauthgamer asked about the sparsifiability of arbitrary constraint satisfaction ... more >>>

We present the first algorithms for polynomial identity testing (PIT) of read-$4$ arithmetic formulas in the non-multilinear setting. Specifically, we give a polynomial-time PIT algorithm in the whitebox model and a quasi-polynomial-time algorithm in the blackbox model. Since our techniques are based on proving hardness of representation results, we extend ... more >>>