Search Results

Documents authored by Lauria, Massimo

Document
DOI: 10.4230/LIPIcs.SAT.2024.7
MaxSAT Resolution with Inclusion Redundancy

Authors: Ilario Bonacina, Maria Luisa Bonet, and Massimo Lauria

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Popular redundancy rules for SAT are not necessarily sound for MaxSAT. The works of [Bonacina-Bonet-Buss-Lauria'24] and [Ihalainen-Berg-Järvisalo'22] proposed ways to adapt them, but required specific encodings and more sophisticated checks during proof verification. Here, we propose a different way to adapt redundancy rules from SAT to MaxSAT. Our rules do not require specific encodings, their correctness is simpler to check, but they are slightly less expressive. However, the proposed redundancy rules, when added to MaxSAT-Resolution, are already strong enough to capture Branch-and-bound algorithms, enable short proofs of the optimal cost of notable principles (e.g., the Pigeonhole Principle and the Parity Principle), and allow to break simple symmetries (e.g., XOR-ification does not make formulas harder).
Cite as

Ilario Bonacina, Maria Luisa Bonet, and Massimo Lauria. MaxSAT Resolution with Inclusion Redundancy. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bonacina_et_al:LIPIcs.SAT.2024.7,
  author =	{Bonacina, Ilario and Bonet, Maria Luisa and Lauria, Massimo},
  title =	{{MaxSAT Resolution with Inclusion Redundancy}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.7},
  URN =		{urn:nbn:de:0030-drops-205298},
  doi =		{10.4230/LIPIcs.SAT.2024.7},
  annote =	{Keywords: MaxSAT, Redundancy, MaxSAT resolution, Branch-and-bound, Pigeonhole principle, Parity Principle}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.23
On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares

Authors: Ilario Bonacina, Nicola Galesi, and Massimo Lauria

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
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.
Cite as

Ilario Bonacina, Nicola Galesi, and Massimo Lauria. On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 23:1-23:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bonacina_et_al:LIPIcs.MFCS.2022.23,
  author =	{Bonacina, Ilario and Galesi, Nicola and Lauria, Massimo},
  title =	{{On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{23:1--23:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.23},
  URN =		{urn:nbn:de:0030-drops-168211},
  doi =		{10.4230/LIPIcs.MFCS.2022.23},
  annote =	{Keywords: polynomial calculus, sum-of-squares, roots of unity, knapsack}
}
Document
DOI: 10.4230/LIPIcs.CCC.2021.40
The Power of Negative Reasoning

Authors: Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov

Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)

Abstract
Semialgebraic proof systems have been studied extensively in proof complexity since the late 1990s to understand the power of Gröbner basis computations, linear and semidefinite programming hierarchies, and other methods. Such proof systems are defined alternately with only the original variables of the problem and with special formal variables for positive and negative literals, but there seems to have been no study how these different definitions affect the power of the proof systems. We show for Nullstellensatz, polynomial calculus, Sherali-Adams, and sums-of-squares that adding formal variables for negative literals makes the proof systems exponentially stronger, with respect to the number of terms in the proofs. These separations are witnessed by CNF formulas that are easy for resolution, which establishes that polynomial calculus, Sherali-Adams, and sums-of-squares cannot efficiently simulate resolution without having access to variables for negative literals.
Cite as

Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov. The Power of Negative Reasoning. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 40:1-40:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{derezende_et_al:LIPIcs.CCC.2021.40,
  author =	{de Rezende, Susanna F. and Lauria, Massimo and Nordstr\"{o}m, Jakob and Sokolov, Dmitry},
  title =	{{The Power of Negative Reasoning}},
  booktitle =	{36th Computational Complexity Conference (CCC 2021)},
  pages =	{40:1--40:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-193-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{200},
  editor =	{Kabanets, Valentine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.40},
  URN =		{urn:nbn:de:0030-drops-143140},
  doi =		{10.4230/LIPIcs.CCC.2021.40},
  annote =	{Keywords: Proof complexity, Polynomial calculus, Nullstellensatz, Sums-of-squares, Sherali-Adams}
}
Document
DOI: 10.4230/LIPIcs.CCC.2017.2
Graph Colouring is Hard for Algorithms Based on Hilbert's Nullstellensatz and Gröbner Bases

Authors: Massimo Lauria and Jakob Nordström

Published in: LIPIcs, Volume 79, 32nd Computational Complexity Conference (CCC 2017)

Abstract
We consider the graph k-colouring problem encoded as a set of polynomial equations in the standard way. We prove that there are bounded-degree graphs that do not have legal k-colourings but for which the polynomial calculus proof system defined in [Clegg et al. '96, Alekhnovich et al. '02] requires linear degree, and hence exponential size, to establish this fact. This implies a linear degree lower bound for any algorithms based on Gröbner bases solving graph k-colouring} using this encoding. The same bound applies also for the algorithm studied in a sequence of papers [De Loera et al. '08, '09, '11, '15] based on Hilbert's Nullstellensatz proofs for a slightly different encoding, thus resolving an open problem mentioned, e.g., in [De Loera et al. '09] and [Li et al. '16]. We obtain our results by combining the polynomial calculus degree lower bound for functional pigeonhole principle (FPHP) formulas over bounded-degree bipartite graphs in [Miksa and Nordström '15] with a reduction from FPHP to k-colouring derivable by polynomial calculus in constant degree.
Cite as

Massimo Lauria and Jakob Nordström. Graph Colouring is Hard for Algorithms Based on Hilbert's Nullstellensatz and Gröbner Bases. In 32nd Computational Complexity Conference (CCC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 79, pp. 2:1-2:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{lauria_et_al:LIPIcs.CCC.2017.2,
  author =	{Lauria, Massimo and Nordstr\"{o}m, Jakob},
  title =	{{Graph Colouring is Hard for Algorithms Based on Hilbert's Nullstellensatz and Gr\"{o}bner Bases}},
  booktitle =	{32nd Computational Complexity Conference (CCC 2017)},
  pages =	{2:1--2:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-040-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{79},
  editor =	{O'Donnell, Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2017.2},
  URN =		{urn:nbn:de:0030-drops-75410},
  doi =		{10.4230/LIPIcs.CCC.2017.2},
  annote =	{Keywords: proof complexity, Nullstellensatz, Gr\"{o}bner basis, polynomial calculus, cutting planes, colouring}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.35
Semantic Versus Syntactic Cutting Planes

Authors: Yuval Filmus, Pavel Hrubeš, and Massimo Lauria

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
In this paper, we compare the strength of the semantic and syntactic version of the cutting planes proof system. First, we show that the lower bound technique of Pudlák applies also to semantic cutting planes: the proof system has feasible interpolation via monotone real circuits, which gives an exponential lower bound on lengths of semantic cutting planes refutations. Second, we show that semantic refutations are stronger than syntactic ones. In particular, we give a formula for which any refutation in syntactic cutting planes requires exponential length, while there is a polynomial length refutation in semantic cutting planes. In other words, syntactic cutting planes does not p-simulate semantic cutting planes. We also give two incompatible integer inequalities which require exponential length refutation in syntactic cutting planes. Finally, we pose the following problem, which arises in connection with semantic inference of arity larger than two: can every multivariate non-decreasing real function be expressed as a composition of non-decreasing real functions in two variables?
Cite as

Yuval Filmus, Pavel Hrubeš, and Massimo Lauria. Semantic Versus Syntactic Cutting Planes. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 35:1-35:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{filmus_et_al:LIPIcs.STACS.2016.35,
  author =	{Filmus, Yuval and Hrube\v{s}, Pavel and Lauria, Massimo},
  title =	{{Semantic Versus Syntactic Cutting Planes}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{35:1--35:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.35},
  URN =		{urn:nbn:de:0030-drops-57367},
  doi =		{10.4230/LIPIcs.STACS.2016.35},
  annote =	{Keywords: proof complexity, cutting planes, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.CCC.2015.448
Tight Size-Degree Bounds for Sums-of-Squares Proofs

Authors: Massimo Lauria and Jakob Nordström

Published in: LIPIcs, Volume 33, 30th Conference on Computational Complexity (CCC 2015)

Abstract
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 the n^O(d) running time obtained by using the Lasserre semidefinite programming relaxations to find degree-d SOS proofs is optimal up to constant factors in the exponent. We establish this result by combining NP-reductions expressible as low-degree SOS derivations with the idea of relativizing CNF formulas in [Krajicek '04] and [Dantchev and Riis '03], and then applying a restriction argument as in [Atserias, Müller, and Oliva '13] and [Atserias, Lauria, and Nordstrom '14]. This yields a generic method of amplifying SOS degree lower bounds to size lower bounds, and also generalizes the approach in [ALN14] to obtain size lower bounds for the proof systems resolution, polynomial calculus, and Sherali-Adams from lower bounds on width, degree, and rank, respectively.
Cite as

Massimo Lauria and Jakob Nordström. Tight Size-Degree Bounds for Sums-of-Squares Proofs. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 448-466, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{lauria_et_al:LIPIcs.CCC.2015.448,
  author =	{Lauria, Massimo and Nordstr\"{o}m, Jakob},
  title =	{{Tight Size-Degree Bounds for Sums-of-Squares Proofs}},
  booktitle =	{30th Conference on Computational Complexity (CCC 2015)},
  pages =	{448--466},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-81-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{33},
  editor =	{Zuckerman, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2015.448},
  URN =		{urn:nbn:de:0030-drops-50736},
  doi =		{10.4230/LIPIcs.CCC.2015.448},
  annote =	{Keywords: Proof complexity, resolution, Lasserre, Positivstellensatz, sums-of-squares, SOS, semidefinite programming, size, degree, rank, clique, lower bound}
}
Document
DOI: 10.4230/LIPIcs.STACS.2014.300
From Small Space to Small Width in Resolution

Authors: Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström, and Marc Vinyals

Published in: LIPIcs, Volume 25, 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)

Abstract
In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of 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 from finite model theory. We give an alternative, completely elementary, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutation -- previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.
Cite as

Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström, and Marc Vinyals. From Small Space to Small Width in Resolution. In 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 25, pp. 300-311, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{filmus_et_al:LIPIcs.STACS.2014.300,
  author =	{Filmus, Yuval and Lauria, Massimo and Miksa, Mladen and Nordstr\"{o}m, Jakob and Vinyals, Marc},
  title =	{{From Small Space to Small Width in Resolution}},
  booktitle =	{31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)},
  pages =	{300--311},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-65-1},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{25},
  editor =	{Mayr, Ernst W. and Portier, Natacha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2014.300},
  URN =		{urn:nbn:de:0030-drops-44661},
  doi =		{10.4230/LIPIcs.STACS.2014.300},
  annote =	{Keywords: proof complexity, resolution, width, space, polynomial calculus, PCR}
}
Document
DOI: 10.4230/DagSemProc.10061.4
Hardness of Parameterized Resolution

Authors: Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria

Published in: Dagstuhl Seminar Proceedings, Volume 10061, Circuits, Logic, and Games (2010)

Abstract
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 main results: 1) We introduce a purely combinatorial approach to obtain lower bounds to the proof size in tree-like Parameterized Resolution. For this we devise a new asymmetric Prover-Delayer game which characterizes proofs in (parameterized) tree-like Resolution. By exhibiting good Delayer strategies we then show lower bounds for the pigeonhole principle as well as the order principle. 2) Interpreting a well-known FPT algorithm for vertex cover as a DPLL procedure for Parameterized Resolution, we devise a proof search algorithm for Parameterized Resolution and show that tree-like Parameterized Resolution allows short refutations of all parameterized contradictions given as bounded-width CNF's. 3) We answer a question posed by Dantchev, Martin, and Szeider showing that dag-like Parameterized Resolution is not fpt-bounded. We obtain this result by proving that the pigeonhole principle requires proofs of size $n^{Omega(k)}$ in dag-like Parameterized Resolution. For this lower bound we use a different Prover-Delayer game which was developed for Resolution by Pudlák.
Cite as

Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. Hardness of Parameterized Resolution. In Circuits, Logic, and Games. Dagstuhl Seminar Proceedings, Volume 10061, pp. 1-28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:DagSemProc.10061.4,
  author =	{Beyersdorff, Olaf and Galesi, Nicola and Lauria, Massimo},
  title =	{{Hardness of Parameterized Resolution}},
  booktitle =	{Circuits, Logic, and Games},
  pages =	{1--28},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10061},
  editor =	{Benjamin Rossman and Thomas Schwentick and Denis Th\'{e}rien and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10061.4},
  URN =		{urn:nbn:de:0030-drops-25254},
  doi =		{10.4230/DagSemProc.10061.4},
  annote =	{Keywords: Proof complexity, parameterized complexity, Resolution, Prover-Delayer Games}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact