Joshua Grochow, Toniann Pitassi

We introduce a new and very natural algebraic proof system, which has tight connections to (algebraic) circuit complexity. In particular, we show that any super-polynomial lower bound on any Boolean tautology in our proof system implies that the permanent does not have polynomial-size algebraic circuits ($VNP \neq VP$). As a ... more >>>

Michael Forbes, Amir Shpilka, Ben Lee Volk

We formalize a framework of algebraically natural lower bounds for algebraic circuits. Just as with the natural proofs notion of Razborov and Rudich for boolean circuit lower bounds, our notion of algebraically natural lower bounds captures nearly all lower bound techniques known. However, unlike the boolean setting, there has been ... more >>>

Joshua Grochow, Mrinal Kumar, Michael Saks, Shubhangi Saraf

We observe that a certain kind of algebraic proof - which covers essentially all known algebraic circuit lower bounds to date - cannot be used to prove lower bounds against VP if and only if what we call succinct hitting sets exist for VP. This is analogous to the Razborov-Rudich ... more >>>

Prasad Chaugule, Nutan Limaye, Aditya Varre

We present polynomial families complete for the well-studied algebraic complexity classes VF, VBP, VP, and VNP. The polynomial families are based on the homomorphism polynomials studied in the recent works of Durand et al. (2014) and Mahajan et al. (2016). We consider three different variants of graph homomorphisms, namely injective ... more >>>

Iddo Tzameret, Stephen Cook

Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over $GF(2)$ in Hrubes-Tzameret [SICOMP'15]. Specifically, we show that the multiplicativity of the determinant function and the ... more >>>

Yaroslav Alekseev, Dima Grigoriev, Edward Hirsch, Iddo Tzameret

We introduce the `binary value principle' which is a simple subset-sum instance expressing that a natural number written in binary cannot be negative, relating it to central problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, ... more >>>

Pavel Hrubes, Amir Yehudayoff

We define the shadow complexity of a polytope P as the maximum number of vertices in a linear projection of $P$ to the plane. We describe connections to algebraic complexity and to parametrized optimization. We also provide several basic examples and constructions, and develop tools for bounding shadow complexity.

Prerona Chatterjee

The motivating question for this work is a long standing open problem, posed by Nisan (1991), regarding the relative powers of algebraic branching programs (ABPs) and formulas in the non-commutative setting. Even though the general question continues to remain open, we make some progress towards its resolution. To that effect, ... more >>>

Rahul Santhanam, Iddo Tzameret

We propose a diagonalization-based approach to several important questions in proof complexity. We illustrate this approach in the context of the algebraic proof system IPS and in the context of propositional proof systems more generally.

We give an explicit sequence of CNF formulas $\{\phi_n\}$ such that VNP$\neq$VP iff there are ... more >>>

Nashlen Govindasamy, Tuomas Hakoniemi, Iddo Tzameret

We prove super-polynomial lower bounds on the size of propositional proof systems operating with constant-depth algebraic circuits over fields of zero characteristic. Specifically, we show that the subset-sum variant $\sum_{i,j,k,l\in[n]} z_{ijkl}x_ix_jx_kx_l-\beta = 0$, for Boolean variables, does not have polynomial-size IPS refutations where the refutations are multilinear and written as ... more >>>

Deepanshu Kush, Shubhangi Saraf

In this paper, we prove strengthened lower bounds for constant-depth set-multilinear formulas. More precisely, we show that over any field, there is an explicit polynomial $f$ in VNP defined over $n^2$ variables, and of degree $n$, such that any product-depth $\Delta$ set-multilinear formula computing $f$ has size at least $n^{\Omega ... more >>>

Arkadev Chattopadhyay, Utsab Ghosal, Partha Mukhopadhyay

We establish an $\epsilon$-sensitive hierarchy separation for monotone arithmetic computations. The notion of $\epsilon$-sensitive monotone lower bounds was recently introduced by Hrubes [Computational Complexity'20]. We show the following:

(1) There exists a monotone polynomial over $n$ variables in VNP that cannot be computed by $2^{o(n)}$ size monotone ...
more >>>

Tuomas Hakoniemi , Nutan Limaye, Iddo Tzameret

Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi JACM 2018) offer a general model for

deriving polynomials in an ideal and refuting unsatisfiable propositional formulas, subsuming most standard propositional proof systems. A major approach for lower bounding the size of IPS refutations is the Functional Lower Bound ...
more >>>