Search Results

Documents authored by Bonacina, Ilario

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