All reports by Author Ilario Bonacina:

__
TR22-105
| 18th July 2022
__

Ilario Bonacina, Nicola Galesi, Massimo Lauria#### On vanishing sums of roots of unity in polynomial calculus and sum-of-squares

__
TR22-089
| 18th June 2022
__

Ilario Bonacina, Neil Thapen#### A separation of PLS from PPP

__
TR21-182
| 30th December 2021
__

Ilario Bonacina, Maria Luisa Bonet#### On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems

__
TR16-057
| 11th April 2016
__

Ilario Bonacina#### Total space in Resolution is at least width squared

__
TR15-133
| 12th August 2015
__

Olaf Beyersdorff, Ilario Bonacina, Leroy Chew#### Lower bounds: from circuits to QBF proof systems

__
TR14-146
| 6th November 2014
__

Ilario Bonacina, Nicola Galesi, Tony Huynh, Paul Wollan#### Space proof complexity for random $3$-CNFs via a $(2-\epsilon)$-Hall's Theorem

__
TR14-038
| 24th March 2014
__

Ilario Bonacina, Nicola Galesi, Neil Thapen#### Total space in resolution

Revisions: 1

__
TR12-119
| 24th September 2012
__

Ilario Bonacina, Nicola Galesi#### Pseudo-partitions, Transversality and Locality: A Combinatorial Characterization for the Space Measure in Algebraic Proof Systems

Ilario Bonacina, Nicola Galesi, Massimo Lauria

Vanishing sums of roots of unity can be seen as a natural generalization of knapsack from Boolean variables to variables taking values over the roots of unity. We show that these sums are hard to prove for polynomial calculus and for sum-of-squares, both in terms of degree and size.

more >>>Ilario Bonacina, Neil Thapen

Recently it was shown that PLS is not contained in PPADS (ECCC report TR22-058). We show that this separation already implies that PLS is not contained in PPP. These separations are shown for the decision tree model of TFNP and imply similar separations in the type-2, relativized model.

Important note. ... more >>>

Ilario Bonacina, Maria Luisa Bonet

The propositional proof system Sherali-Adams (SA) has polynomial-size proofs of the pigeonhole principle (PHP). Similarly, the Nullstellensatz (NS) proof system has polynomial size proofs of the bijective (i.e. both functional and onto) pigeonhole principle (ofPHP). We characterize the strength of these algebraic proof systems in terms of Boolean proof systems ... more >>>

Ilario Bonacina

Given an unsatisfiable $k$-CNF formula $\phi$ we consider two complexity measures in Resolution: width and total space. The width is the minimal $W$ such that there exists a Resolution refutation of $\phi$ with clauses of at most $W$ literals. The total space is the minimal size $T$ of a memory ... more >>>

Olaf Beyersdorff, Ilario Bonacina, Leroy Chew

A general and long-standing belief in the proof complexity community asserts that there is a close connection between progress in lower bounds for Boolean circuits and progress in proof size lower bounds for strong propositional proof systems. Although there are famous examples where a transfer from ideas and techniques from ... more >>>

Ilario Bonacina, Nicola Galesi, Tony Huynh, Paul Wollan

We investigate the space complexity of refuting $3$-CNFs in Resolution and algebraic systems. No lower bound for refuting any family of $3$-CNFs was previously known for the total space in resolution or for the monomial space in algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a ... more >>>

Ilario Bonacina, Nicola Galesi, Neil Thapen

We show $\Omega(n^2)$ lower bounds on the total space used in resolution refutations of random $k$-CNFs over $n$ variables, and of the graph pigeonhole principle and the bit pigeonhole principle for $n$ holes. This answers the long-standing open problem of whether there are families of $k$-CNF formulas of size $O(n)$ ... more >>>

Ilario Bonacina, Nicola Galesi

We devise a new combinatorial characterization for proving space lower bounds in algebraic systems like Polynomial Calculus (Pc) and Polynomial Calculus with Resolution (Pcr). Our method can be thought as a Spoiler-Duplicator game, which is capturing boolean reasoning on polynomials instead that clauses as in the case of Resolution. Hence, ... more >>>