Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

All reports by Author Iddo Tzameret:

TR22-055 | 23rd April 2022
Nashlen Govindasamy, Tuomas Hakoniemi, Iddo Tzameret

Simple Hard Instances for Low-Depth Algebraic Proofs

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 >>>

TR21-138 | 23rd September 2021
Rahul Santhanam, Iddo Tzameret

Iterated Lower Bound Formulas: A Diagonalization-Based Approach to Proof Complexity

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 >>>

TR19-142 | 23rd October 2019
Yaroslav Alekseev, Dima Grigoriev, Edward Hirsch, Iddo Tzameret

Semi-Algebraic Proofs, IPS Lower Bounds and the $\tau$-Conjecture: Can a Natural Number be Negative?

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 >>>

TR18-184 | 5th November 2018
Iddo Tzameret, Stephen Cook

Uniform, Integral and Feasible Proofs for the Determinant Identities

Revisions: 1

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 >>>

TR18-117 | 23rd June 2018
Fedor Part, Iddo Tzameret

Resolution with Counting: Lower Bounds over Different Moduli

Revisions: 2

Resolution over linear equations (introduced in [RT08]) emerged recently as an important object of study. This refutation system, denoted Res(lin$_R$), operates with disjunction of linear equations over a ring $R$. On the one hand, the system captures a natural ``minimal'' extension of resolution in which efficient counting can be achieved; ... more >>>

TR16-101 | 1st July 2016
Toniann Pitassi, Iddo Tzameret

Algebraic Proof Complexity: Progress, Frontiers and Challenges

We survey recent progress in the proof complexity of strong proof systems and its connection to algebraic circuit complexity, showing how the synergy between the two gives rise to new approaches to fundamental open questions, solutions to old problems, and new directions of research. In particular, we focus on tight ... more >>>

TR16-098 | 16th June 2016
Michael Forbes, Amir Shpilka, Iddo Tzameret, Avi Wigderson

Proof Complexity Lower Bounds from Algebraic Circuit Complexity

We give upper and lower bounds on the power of subsystems of the Ideal Proof System (IPS), the algebraic proof system recently proposed by Grochow and Pitassi, where the circuits comprising the proof come from various restricted algebraic circuit classes. This mimics an established research direction in the ... more >>>

TR15-134 | 19th August 2015
Fu Li, Iddo Tzameret, Zhengyu Wang

Characterizing Propositional Proofs as Non-Commutative Formulas

Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional-calculus (i.e., Frege) proof is any proof starting from a set of axioms and deriving new Boolean formulas using a fixed set of sound derivation rules. Establishing any super-polynomial size lower bound on Frege proofs (in terms of the ... more >>>

TR13-185 | 24th December 2013
Fu Li, Iddo Tzameret

Generating Matrix Identities and Proof Complexity Lower Bounds

Revisions: 3

Motivated by the fundamental lower bounds questions in proof complexity, we investigate the complexity of generating identities of matrix rings, and related problems. Specifically, for a field $\mathbb{F}$ let $A$ be a non-commutative (associative) $\mathbb{F}$-algebra (e.g., the algebra Mat$_d(\mathbb{F})\;$ of $d\times d$ matrices over $\mathbb{F}$). We say that a non-commutative ... more >>>

TR13-070 | 4th May 2013
Iddo Tzameret

On Sparser Random 3SAT Refutation Algorithms and Feasible Interpolation

Revisions: 1

We formalize a combinatorial principle, called the 3XOR principle, due to Feige, Kim and Ofek (2006), as a family of unsatisfiable propositional formulas for which refutations of small size in any propositional proof system that possesses the feasible interpolation property imply an efficient *deterministic* refutation algorithm for random 3SAT with ... more >>>

TR12-028 | 30th March 2012
Eric Allender, George Davie, Luke Friedman, Samuel Hopkins, Iddo Tzameret

Kolmogorov Complexity, Circuits, and the Strength of Formal Theories of Arithmetic

Revisions: 1

Can complexity classes be characterized in terms of efficient reducibility to the (undecidable) set of Kolmogorov-random strings? Although this might seem improbable, a series of papers has recently provided evidence that this may be the case. In particular, it is known that there is a class of problems $C$ defined ... more >>>

TR11-174 | 30th December 2011
Pavel Hrubes, Iddo Tzameret

Short Proofs for the Determinant Identities

Revisions: 1

We study arithmetic proof systems $\mathbb{P}_c(\mathbb{F})$ and $\mathbb{P}_f(\mathbb{F})$ operating with arithmetic circuits and arithmetic formulas, respectively, that prove polynomial identities over a field $\mathbb{F}$. We establish a series of structural theorems about these proof systems, the main one stating that $\mathbb{P}_c(\mathbb{F})$ proofs can be balanced: if a polynomial identity of ... more >>>

TR11-006 | 20th January 2011
Sebastian Müller, Iddo Tzameret

Average-Case Separation in Proof Complexity: Short Propositional Refutations for Random 3CNF Formulas

Revisions: 1

Separating different propositional proof systems---that is, demonstrating that one proof system cannot efficiently simulate another proof system---is one of the main goals of proof complexity. Nevertheless, all known separation results between non-abstract proof systems are for specific families of hard tautologies: for what we know, in the average case all ... more >>>

TR10-097 | 16th June 2010
Iddo Tzameret

Algebraic Proofs over Noncommutative Formulas

Revisions: 1

We study possible formulations of algebraic propositional proof systems operating with noncommutative formulas. We observe that a simple formulation gives rise to systems at least as strong as Frege--yielding a semantic way to define a Cook-Reckhow (i.e., polynomially verifiable) algebraic analogue of Frege proofs, different from that given in Buss ... more >>>

TR07-078 | 11th August 2007
Ran Raz, Iddo Tzameret

Resolution over Linear Equations and Multilinear Proofs

We develop and study the complexity of propositional proof systems of varying strength extending resolution by allowing it to operate with disjunctions of linear equations instead of clauses. We demonstrate polynomial-size refutations for hard tautologies like the pigeonhole principle, Tseitin graph tautologies and the clique-coloring tautologies in these proof systems. ... more >>>

TR06-001 | 1st January 2006
Ran Raz, Iddo Tzameret

The Strength of Multilinear Proofs

We introduce an algebraic proof system that manipulates multilinear arithmetic formulas. We show that this proof system is fairly strong, even when restricted to multilinear arithmetic formulas of a very small depth. Specifically, we show the following:

1. Algebraic proofs manipulating depth 2 multilinear arithmetic formulas polynomially simulate Resolution, Polynomial ... more >>>

ISSN 1433-8092 | Imprint