6 Search Results for "Bonacina, Ilario"

Document
DOI: 10.4230/LIPIcs.ITCS.2024.48
Proving Unsatisfiability with Hitting Formulas

Authors: Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals

Published in: LIPIcs, Volume 287, 15th Innovations in Theoretical Computer Science Conference (ITCS 2024)

Abstract
A hitting formula is a set of Boolean clauses such that any two of the clauses cannot be simultaneously falsified. Hitting formulas have been studied in many different contexts at least since [Iwama, 1989] and, based on experimental evidence, Peitl and Szeider [Tomás Peitl and Stefan Szeider, 2022] conjectured that unsatisfiable hitting formulas are among the hardest for resolution. Using the fact that hitting formulas are easy to check for satisfiability we make them the foundation of a new static proof system {{rmHitting}}: a refutation of a CNF in {{rmHitting}} is an unsatisfiable hitting formula such that each of its clauses is a weakening of a clause of the refuted CNF. Comparing this system to resolution and other proof systems is equivalent to studying the hardness of hitting formulas. Our first result is that {{rmHitting}} is quasi-polynomially simulated by tree-like resolution, which means that hitting formulas cannot be exponentially hard for resolution and partially refutes the conjecture of Peitl and Szeider. We show that tree-like resolution and {{rmHitting}} are quasi-polynomially separated, while for resolution, this question remains open. For a system that is only quasi-polynomially stronger than tree-like resolution, {{rmHitting}} is surprisingly difficult to polynomially simulate in another proof system. Using the ideas of Raz-Shpilka’s polynomial identity testing for noncommutative circuits [Raz and Shpilka, 2005] we show that {{rmHitting}} is p-simulated by {{rmExtended {{rmFrege}}}}, but we conjecture that much more efficient simulations exist. As a byproduct, we show that a number of static (semi)algebraic systems are verifiable in deterministic polynomial time. We consider multiple extensions of {{rmHitting}}, and in particular a proof system {{{rmHitting}}(⊕)} related to the {{{rmRes}}(⊕)} proof system for which no superpolynomial-size lower bounds are known. {{{rmHitting}}(⊕)} p-simulates the tree-like version of {{{rmRes}}(⊕)} and is at least quasi-polynomially stronger. We show that formulas expressing the non-existence of perfect matchings in the graphs K_{n,n+2} are exponentially hard for {{{rmHitting}}(⊕)} via a reduction to the partition bound for communication complexity. See the full version of the paper for the proofs. They are omitted in this Extended Abstract.
Cite as

Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals. Proving Unsatisfiability with Hitting Formulas. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{filmus_et_al:LIPIcs.ITCS.2024.48,
  author =	{Filmus, Yuval and Hirsch, Edward A. and Riazanov, Artur and Smal, Alexander and Vinyals, Marc},
  title =	{{Proving Unsatisfiability with Hitting Formulas}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{48:1--48:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.48},
  URN =		{urn:nbn:de:0030-drops-195762},
  doi =		{10.4230/LIPIcs.ITCS.2024.48},
  annote =	{Keywords: hitting formulas, polynomial identity testing, query complexity}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.5
Polynomial Calculus for MaxSAT

Authors: Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
MaxSAT is the problem of finding an assignment satisfying the maximum number of clauses in a CNF formula. We consider a natural generalization of this problem to generic sets of polynomials and propose a weighted version of Polynomial Calculus to address this problem. Weighted Polynomial Calculus is a natural generalization of MaxSAT-Resolution and weighted Resolution that manipulates polynomials with coefficients in a finite field and either weights in ℕ or ℤ. We show the soundness and completeness of these systems via an algorithmic procedure. Weighted Polynomial Calculus, with weights in ℕ and coefficients in 𝔽₂, is able to prove efficiently that Tseitin formulas on a connected graph are minimally unsatisfiable. Using weights in ℤ, it also proves efficiently that the Pigeonhole Principle is minimally unsatisfiable.
Cite as

Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy. Polynomial Calculus for MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bonacina_et_al:LIPIcs.SAT.2023.5,
  author =	{Bonacina, Ilario and Bonet, Maria Luisa and Levy, Jordi},
  title =	{{Polynomial Calculus for MaxSAT}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.5},
  URN =		{urn:nbn:de:0030-drops-184670},
  doi =		{10.4230/LIPIcs.SAT.2023.5},
  annote =	{Keywords: Polynomial Calculus, MaxSAT, Proof systems, Algebraic reasoning}
}
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-dev.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.2019.6
Resolution and the Binary Encoding of Combinatorial Principles

Authors: Stefan Dantchev, Nicola Galesi, and Barnaby Martin

Published in: LIPIcs, Volume 137, 34th Computational Complexity Conference (CCC 2019)

Abstract
Res(s) is an extension of Resolution working on s-DNFs. We prove tight n^{Omega(k)} lower bounds for the size of refutations of the binary version of the k-Clique Principle in Res(o(log log n)). Our result improves that of Lauria, Pudlák et al. [Massimo Lauria et al., 2017] who proved the lower bound for Res(1), i.e. Resolution. The exact complexity of the (unary) k-Clique Principle in Resolution is unknown. To prove the lower bound we do not use any form of the Switching Lemma [Nathan Segerlind et al., 2004], instead we apply a recursive argument specific for binary encodings. Since for the k-Clique and other principles lower bounds in Resolution for the unary version follow from lower bounds in Res(log n) for their binary version we start a systematic study of the complexity of proofs in Resolution-based systems for families of contradictions given in the binary encoding. We go on to consider the binary version of the weak Pigeonhole Principle Bin-PHP^m_n for m>n. Using the the same recursive approach we prove the new result that for any delta>0, Bin-PHP^m_n requires proofs of size 2^{n^{1-delta}} in Res(s) for s=o(log^{1/2}n). Our lower bound is almost optimal since for m >= 2^{sqrt{n log n}} there are quasipolynomial size proofs of Bin-PHP^m_n in Res(log n). Finally we propose a general theory in which to compare the complexity of refuting the binary and unary versions of large classes of combinatorial principles, namely those expressible as first order formulae in Pi_2-form and with no finite model.
Cite as

Stefan Dantchev, Nicola Galesi, and Barnaby Martin. Resolution and the Binary Encoding of Combinatorial Principles. In 34th Computational Complexity Conference (CCC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 137, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{dantchev_et_al:LIPIcs.CCC.2019.6,
  author =	{Dantchev, Stefan and Galesi, Nicola and Martin, Barnaby},
  title =	{{Resolution and the Binary Encoding of Combinatorial Principles}},
  booktitle =	{34th Computational Complexity Conference (CCC 2019)},
  pages =	{6:1--6:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-116-0},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{137},
  editor =	{Shpilka, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2019.6},
  URN =		{urn:nbn:de:0030-drops-108287},
  doi =		{10.4230/LIPIcs.CCC.2019.6},
  annote =	{Keywords: Proof complexity, k-DNF resolution, binary encodings, Clique and Pigeonhole principle}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.56
Total Space in Resolution Is at Least Width Squared

Authors: Ilario Bonacina

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
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 used to write down a Resolution refutation of phi where the size of the memory is measured as the total number of literals it can contain. We prove that T = Omega((W - k)^2).
Cite as

Ilario Bonacina. Total Space in Resolution Is at Least Width Squared. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 56:1-56:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bonacina:LIPIcs.ICALP.2016.56,
  author =	{Bonacina, Ilario},
  title =	{{Total Space in Resolution Is at Least Width Squared}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{56:1--56:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.56},
  URN =		{urn:nbn:de:0030-drops-62273},
  doi =		{10.4230/LIPIcs.ICALP.2016.56},
  annote =	{Keywords: Resolution, width, total space}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2015.248
Strong ETH and Resolution via Games and the Multiplicity of Strategies

Authors: Ilario Bonacina and Navid Talebanfard

Published in: LIPIcs, Volume 43, 10th International Symposium on Parameterized and Exact Computation (IPEC 2015)

Abstract
We consider a restriction of the Resolution proof system in which at most a fixed number of variables can be resolved more than once along each refutation path. This system lies between regular Resolution, in which no variable can be resolved more than once along any path, and general Resolution where there is no restriction on the number of such variables. We show that when the number of re-resolved variables is not too large, this proof system is consistent with the Strong Exponential Time Hypothesis (SETH). More precisely for large n and k we show that there are unsatisfiable k-CNF formulas which require Resolution refutations of size 2^{(1 - epsilon_k)n}, where n is the number of variables and epsilon_k=~O(k^{-1/5}), whenever in each refutation path we only allow at most ~O(k^{-1/5})n variables to be resolved multiple times. However, these re-resolved variables along different paths do not need to be the same. Prior to this work, the strongest proof system shown to be consistent with SETH was regular Resolution [Beck and Impagliazzo, STOC'13]. This work strengthens that result and gives a different and conceptually simpler game-theoretic proof for the case of regular Resolution.
Cite as

Ilario Bonacina and Navid Talebanfard. Strong ETH and Resolution via Games and the Multiplicity of Strategies. In 10th International Symposium on Parameterized and Exact Computation (IPEC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 43, pp. 248-257, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bonacina_et_al:LIPIcs.IPEC.2015.248,
  author =	{Bonacina, Ilario and Talebanfard, Navid},
  title =	{{Strong ETH and Resolution via Games and the Multiplicity of Strategies}},
  booktitle =	{10th International Symposium on Parameterized and Exact Computation (IPEC 2015)},
  pages =	{248--257},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-92-7},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{43},
  editor =	{Husfeldt, Thore and Kanj, Iyad},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2015.248},
  URN =		{urn:nbn:de:0030-drops-55876},
  doi =		{10.4230/LIPIcs.IPEC.2015.248},
  annote =	{Keywords: Strong Exponential Time Hypothesis, resolution, proof systems}
}
  • Refine by Author
  • 4 Bonacina, Ilario
  • 2 Galesi, Nicola
  • 1 Bonet, Maria Luisa
  • 1 Dantchev, Stefan
  • 1 Filmus, Yuval
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Proof complexity
  • 1 Computing methodologies → Representation of polynomials
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Complexity theory and logic

  • Refine by Keyword
  • 1 Algebraic reasoning
  • 1 Clique and Pigeonhole principle
  • 1 MaxSAT
  • 1 Polynomial Calculus
  • 1 Proof complexity
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 1 2015
  • 1 2016
  • 1 2019
  • 1 2022
  • 1 2023
  • Show More...

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