All reports by Author Massimo Lauria:

__
TR24-045
| 6th March 2024
__

Ilario Bonacina, Maria Luisa Bonet, Sam Buss, Massimo Lauria#### Redundancy for MaxSAT

__
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

__
TR15-053
| 7th April 2015
__

Massimo Lauria, Jakob Nordström#### Tight Size-Degree Bounds for Sums-of-Squares Proofs

__
TR14-118
| 9th September 2014
__

Albert Atserias, Massimo Lauria, Jakob Nordström#### Narrow Proofs May Be Maximally Long

__
TR14-081
| 13th June 2014
__

Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, Marc Vinyals#### From Small Space to Small Width in Resolution

__
TR13-038
| 13th March 2013
__

Massimo Lauria, Pavel Pudlak, Vojtech Rodl, Neil Thapen#### The complexity of proving that a graph is Ramsey

Revisions: 1

__
TR12-161
| 20th November 2012
__

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria#### A Characterization of Tree-Like Resolution Size

__
TR12-132
| 21st October 2012
__

Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, Neil Thapen#### Space Complexity in Polynomial Calculus

__
TR12-124
| 29th September 2012
__

Massimo Lauria#### A rank lower bound for cutting planes proofs of Ramsey Theorem

__
TR10-198
| 13th December 2010
__

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, Alexander Razborov#### Parameterized Bounded-Depth Frege is Not Optimal

__
TR10-153
| 7th October 2010
__

Lorenzo Carlucci, Nicola Galesi, Massimo Lauria#### Paris-Harrington tautologies

Revisions: 2

__
TR10-081
| 10th May 2010
__

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria#### A Lower Bound for the Pigeonhole Principle in Tree-like Resolution by Asymmetric Prover-Delayer Games

__
TR10-059
| 8th April 2010
__

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria#### Hardness of Parameterized Resolution

__
TR09-137
| 14th December 2009
__

Massimo Lauria#### Random CNFs require spacious Polynomial Calculus refutations

Comments: 1

__
TR09-035
| 26th March 2009
__

Nicola Galesi, Massimo Lauria#### On the Automatizability of Polynomial Calculus

__
TR07-041
| 20th April 2007
__

Nicola Galesi, Massimo Lauria#### Extending Polynomial Calculus to $k$-DNF Resolution

Revisions: 1

Ilario Bonacina, Maria Luisa Bonet, Sam Buss, Massimo Lauria

The concept of redundancy in SAT lead to more expressive and powerful proof search techniques, e.g. able to express various inprocessing techniques, and to interesting hierarchies of proof systems [Heule et.al’20, Buss-Thapen’19].

We propose a general way to integrate redundancy rules in MaxSAT, that is we define MaxSAT variants of ...
more >>>

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 >>>Massimo Lauria, Jakob Nordström

We exhibit families of 4-CNF formulas over n variables that have sums-of-squares (SOS) proofs of unsatisfiability of degree (a.k.a. rank) d but require SOS proofs of size n^{Omega(d)} for values of d = d(n) from constant all the way up to n^{delta} for some universal constant delta. This shows that ... more >>>

Albert Atserias, Massimo Lauria, Jakob Nordström

We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n^Omega(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size n^O(w) is essentially tight. ... more >>>

Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, Marc Vinyals

In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of CNF formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools ... more >>>

Massimo Lauria, Pavel Pudlak, Vojtech Rodl, Neil Thapen

We say that a graph with $n$ vertices is $c$-Ramsey if it does not contain either a clique or an independent set of size $c \log n$. We define a CNF formula which expresses this property for a graph $G$. We show a superpolynomial lower bound on the length of ... more >>>

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

We explain an asymmetric Prover-Delayer game which precisely characterizes proof size in tree-like Resolution. This game was previously described in a parameterized complexity context to show lower bounds for parameterized formulas and for the classical pigeonhole principle. The main point of this note is to show that the asymmetric game ... more >>>

Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, Neil Thapen

During the last decade, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important issue in SAT solving, and so research has mostly focused on weak systems ... more >>>

Massimo Lauria

Ramsey Theorem is a cornerstone of combinatorics and logic. In its

simplest formulation it says that there is a function $r$ such that

any simple graph with $r(k,s)$ vertices contains either a clique of

size $k$ or an independent set of size $s$. We study the complexity

of proving upper ...
more >>>

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, Alexander Razborov

A general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that framework the parameterized version of any proof system is not fpt-bounded for some technical reasons, but we remark that this question becomes much more interesting if we restrict ourselves to those parameterized contradictions ... more >>>

Lorenzo Carlucci, Nicola Galesi, Massimo Lauria

We initiate the study of the proof complexity of propositional encoding of (weak cases of) concrete independence results. In particular we study the proof complexity of Paris-Harrington's Large Ramsey Theorem. We prove a conditional lower bound in Resolution and a quasipolynomial upper bound in bounded-depth Frege.

more >>>Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

In this note we show that the asymmetric Prover-Delayer game developed by Beyersdorff, Galesi, and Lauria (ECCC TR10-059) for Parameterized Resolution is also applicable to other tree-like proof systems. In particular, we use this asymmetric Prover-Delayer game to show a lower bound of the form $2^{\Omega(n\log n)}$ for the pigeonhole ... more >>>

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

Parameterized Resolution and, moreover, a general framework for parameterized proof complexity was introduced by Dantchev, Martin, and Szeider (FOCS'07). In that paper, Dantchev et al. show a complexity gap in tree-like Parameterized Resolution for propositional formulas arising from translations of first-order principles.

We broadly investigate Parameterized Resolution obtaining the following ...
more >>>

Massimo Lauria

We study the space required by Polynomial Calculus refutations of random $k$-CNFs. We are interested in how many monomials one needs to keep in memory to carry on a refutation. More precisely we show that for $k \geq 4$ a refutation of a random $k$-CNF of $\Delta n$ clauses and ... more >>>

Nicola Galesi, Massimo Lauria

We prove that Polynomial Calculus and Polynomial Calculus with Resolution are not automatizable, unless W[P]-hard problems are fixed parameter tractable by one-side error randomized algorithms. This extends to Polynomial Calculus the analogous result obtained for Resolution by Alekhnovich and Razborov (SIAM J. Computing, 38(4), 2008).

more >>>Nicola Galesi, Massimo Lauria

We introduce an algebraic proof system Pcrk, which combines together {\em Polynomial Calculus} (Pc) and {\em $k$-DNF Resolution} (Resk).

This is a natural generalization to Resk of the well-known {\em Polynomial Calculus with Resolution} (Pcr) system which combines together Pc and Resolution.

We study the complexity of proofs in such ... more >>>