In recent years there has been an increasing interest in studying proof systems stronger than Resolution, with the aim of building more efficient SAT solvers based on them. In defining these proof systems, we try to find a balance between the power of the proof system (the size of the proofs required to refute a formula) and the difficulty of finding the proofs.
In this paper we consider the proof systems circular Resolution, Sherali-Adams, Nullstellensatz and Weighted Resolution and we study their relative power from a theoretical perspective. We prove that circular Resolution, Sherali-Adams and Weighted Resolution are polynomially equivalent proof systems. We also prove that Nullstellensatz is polynomially equivalent to a restricted version of Weighted Resolution. The equivalences carry on also for versions of the systems where the coefficients/weights are expressed in unary.
The practical interest in these systems comes from the fact that they admit efficient algorithms to find proofs in case these have small width/degree.
@article{BBL24-jair,title={Weighted, circular and semi-algebraic proofs},author={Bonacina, Ilario and Bonet, Maria Luisa and Levy, Jordi},journal={Journal of Artificial Intelligence Research (JAIR)},volume={79},pages={447--482},month=feb,year={2024},doi={10.1613/jair.1.15075},}
2023
On vanishing sums of roots of unity in polynomial calculus and sum-of-squares
Ilario
Bonacina
,
Nicola
Galesi
,
and
Massimo
Lauria
We introduce a novel take on sum-of-squares that is able to reason with complex numbers and still make use of polynomial inequalities. This proof system might be of independent interest since it allows to represent multivalued domains both with Boolean and Fourier encoding. We show degree and size lower bounds in this system for a natural generalization of knapsack: the vanishing sums of roots of unity. These lower bounds naturally apply to polynomial calculus as-well.
@article{BGL23-compcompl,author={Bonacina, Ilario and Galesi, Nicola and Lauria, Massimo},title={On vanishing sums of roots of unity in polynomial calculus and sum-of-squares},journal={computational complexity},volume={32},number={2},pages={12},year={2023},doi={10.1007/S00037-023-00242-Z},}
Polynomial Calculus for MaxSAT
Ilario
Bonacina
,
Maria Luisa
Bonet
,
and
Jordi
Levy
In Proceedings of SAT’23 (26th International Conference on Theory and Applications of Satisfiability Testing) , Feb 2023
@inproceedings{BBL23-sat,author={Bonacina, Ilario and Bonet, Maria Luisa and Levy, Jordi},title={Polynomial Calculus for MaxSAT},booktitle={SAT'23 (26th International Conference on Theory and Applications of Satisfiability Testing)},volume={},pages={},year={2023},doi={10.4230/LIPIcs.SAT.2023.5},}
2022
On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares
Ilario
Bonacina
,
Nicola
Galesi
,
and
Massimo
Lauria
In Proceedings of MFCS’22 (47th International Symposium on Mathematical Foundations of Computer
Science) , Feb 2022
@inproceedings{BGL22-mfcs,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={MFCS'22 (47th International Symposium on Mathematical Foundations of Computer
Science)},volume={241},pages={23:1--23:15},year={2022},doi={10.4230/LIPIcs.MFCS.2022.23},}
On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems
Ilario
Bonacina
,
and
Maria Luisa
Bonet
In Proceedings of LICS ’22 (37th Annual ACM/IEEE Symposium on Logic in Computer Science) , Feb 2022
@inproceedings{BB22-lics,title={On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems},author={Bonacina, Ilario and Bonet, Maria Luisa},booktitle={LICS '22 (37th Annual {ACM/IEEE} Symposium on Logic in Computer Science)},doi={10.1145/3531130.3533344},pages={25:1--25:12},year={2022},}
2021
Clique Is Hard on Average for Regular Resolution
Albert
Atserias
,
Ilario
Bonacina
,
Susanna F.
De Rezende
, and
3 more authors
We prove that for k≪n^1/4 regular resolution requires
length n^Ω(k) to establish that an Erdos–Renyi graph with appropriately
chosen edge density does not contain a k-clique.
This lower bound is optimal up to the multiplicative constant in the exponent
and also implies unconditional n^Ω(k) lower bounds on running time for several
state-of-the-art algorithms for finding maximum cliques in graphs.
@article{ABDLNR21-jacm,author={Atserias, Albert and Bonacina, Ilario and De Rezende, Susanna F. and Lauria, Massimo and Nordstr\"{o}m, Jakob and Razborov, Alexander},doi={10.1145/3449352},journal={Journal of the ACM (JACM)},number={4},pages={1--26},publisher={Association for Computing Machinery},title={Clique Is Hard on Average for Regular Resolution},volume={68},year={2021},}
2020
Frege Systems for Quantified Boolean Logic
Olaf
Beyersdorff
,
Ilario
Bonacina
,
Leroy
Chew
, and
1 more author
We define and investigate Frege systems for quantified Boolean formulas (QBF).
For these new proof systems, we develop a lower bound technique that directly
lifts circuit lower bounds for a circuit class C to the QBF Frege system operating
with lines from C . Such a direct transfer from circuit to proof complexity
lower bounds has often been postulated for propositional systems but had not been
formally established in such generality for any proof systems prior to this work.
This leads to strong lower bounds for restricted versions of QBF Frege, in particular
an exponential lower bound for QBF Frege systems operating with AC0[p] circuits.
In contrast, any non-trivial lower bound for propositional AC0[p]-Frege constitutes
a major open problem.
Improving these lower bounds to unrestricted QBF Frege tightly corresponds to the
major problems in circuit complexity and propositional proof complexity.
In particular, proving a lower bound for QBF Frege systems operating with arbitrary
P/poly circuits is equivalent to either showing a lower bound for P/poly or for
propositional extended Frege (which operates with P/poly circuits).
We also compare our new QBF Frege systems to standard sequent calculi for QBF and
establish a correspondence to intuitionistic bounded arithmetic.
@article{BBCP20-jacm,author={Beyersdorff, Olaf and Bonacina, Ilario and Chew, Leroy and Pich, Jan},doi={10.1145/3381881},journal={Journal of the ACM (JACM)},number={2},pages={1--36},title={Frege Systems for Quantified Boolean Logic},volume={67},year={2020},}
2018
Clique is Hard on Average for Regular Resolution
Albert
Atserias
,
Ilario
Bonacina
,
Susanna F.
de Rezende
, and
3 more authors
In Proceedings of STOC’18 (50th Annual ACM SIGACT Symposium on Theory of Computing) , Feb 2018
@inproceedings{ABDLNR18-stoc,author={Atserias, Albert and Bonacina, Ilario and de\ Rezende, Susanna F. and Lauria, Massimo and Nordstr\"{o}m, Jakob and Razborov, Alexander},booktitle={STOC'18 (50th Annual ACM SIGACT Symposium on Theory of Computing)},doi={10.1145/3188745.3188856},numpages={12},pages={866--877},title={Clique is Hard on Average for Regular Resolution},year={2018},}
2017
Strong ETH and Resolution via Games and the Multiplicity of Strategies
We consider a proof system intermediate between regular Resolution, in which no variable can be resolved more than once along any refutation path, and general Resolution. We call }}\backslashdelta }}-regular Resolution such system, in which at most a fraction }}\backslashdelta }}of the variables can be resolved more than once along each refutation path (however, the re-resolved variables along different paths do not need to be the same). We show that when for }}\backslashdelta }}not too large, }}\backslashdelta }}-regular Resolution 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 }}\backslashdelta }}-regular Resolution refutations of size }}2\^{(1 - \backslashepsilon _k)n}}}, where n is the number of variables and }}\backslashepsilon _k=\backslashwidetilde{O}(k\^{-1/4})}}and }}\backslashdelta =\backslashwidetilde{O}(k\^{-1/4})}}is the number of variables that can be resolved multiple times.
@article{BT16-algorithmica,author={Bonacina, Ilario and Talebanfard, Navid},title={Strong {ETH} and Resolution via Games and the Multiplicity of Strategies},doi={10.1007/s00453-016-0228-6},isbn={1432-0541},journal={Algorithmica},number={1},pages={29--41},volume={79},year={2017},}
@article{BBGHMW17-infocomp,author={Bennett, Patrick and Bonacina, Ilario and Galesi, Nicola and Huynh, Tony and Molloy, Mike and Wollan, Paul},title={Space proof complexity for random $3$-{CNF}s},doi={10.1016/j.ic.2017.06.003},journal={Information and Computation},pages={165--176},volume={255},year={2017},}
2016
Improving resolution width lower bounds for k-CNFs with applications to the Strong Exponential Time Hypothesis
@article{BT16-ipl,author={Bonacina, Ilario and Talebanfard, Navid},doi={10.1016/j.ipl.2015.09.013},journal={Inf. Process. Lett.},number={2},pages={120--124},title={Improving resolution width lower bounds for k-CNFs with applications to the Strong Exponential Time Hypothesis},volume={116},year={2016},}
Improving resolution width lower bounds for k-CNFs with applications to the Strong Exponential Time Hypothesis
@article{BT16-ipl-old,author={Bonacina, Ilario and Talebanfard, Navid},doi={10.1016/j.ipl.2015.09.013},journal={Inf. Process. Lett.},number={2},pages={120--124},title={Improving resolution width lower bounds for k-CNFs with applications to the Strong Exponential Time Hypothesis},volume={116},year={2016},}
@article{BGT16-siamjcomp,author={Bonacina, Ilario and Galesi, Nicola and Thapen, Neil},doi={10.1137/15M1023269},journal={SIAM J. Comput.},month=jan,number={5},pages={1894--1909},title={{Total Space in Resolution}},volume={45},year={2016},}
Total Space in Resolution is at Least Width Squared
Ilario
Bonacina
In Proceedings of ICALP’16 (43rd International Colloquium on Automata, Languages, and Programming) , Jan 2016
@inproceedings{Bon16-icalp,author={Bonacina, Ilario},booktitle={ICALP'16 (43rd International Colloquium on Automata, Languages, and Programming)},doi={10.4230/LIPIcs.ICALP.2016.56},pages={56:1--56:13},title={Total Space in Resolution is at Least Width Squared},volume={55},year={2016},}
Lower Bounds: From Circuits to QBF Proof Systems
Olaf
Beyersdorff
,
Ilario
Bonacina
,
and
Leroy
Chew
In Proceedings of ITCS’16 (7th Conference on Innovations in Theoretical Computer Science) , Jan 2016
@inproceedings{BBC16-itcs,author={Beyersdorff, Olaf and Bonacina, Ilario and Chew, Leroy},booktitle={ITCS'16 (7th Conference on Innovations in Theoretical Computer Science)},doi={10.1145/2840728.2840740},pages={249--260},title={Lower Bounds: From Circuits to {QBF} Proof Systems},year={2016},}
2015
A Framework for Space Complexity in Algebraic Proof Systems
@article{BG15-jacm,author={Bonacina, Ilario and Galesi, Nicola},doi={10.1145/2699438},journal={Journal of the ACM (J. ACM)},number={3},pages={1--20},title={A Framework for Space Complexity in Algebraic Proof Systems},volume={62},year={2015},}
Strong ETH and Resolution via Games and the Multiplicity of Strategies
Ilario
Bonacina
,
and
Navid
Talebanfard
In Proceedings of IPEC’15 (10th International Symposium on Parameterized and Exact Computation) , Jan 2015
@inproceedings{BT15-ipec,author={Bonacina, Ilario and Talebanfard, Navid},booktitle={IPEC'15 (10th International Symposium on Parameterized and Exact Computation)},doi={10.4230/LIPIcs.IPEC.2015.248},pages={248--257},title={Strong {ETH} and Resolution via Games and the Multiplicity of Strategies},year={2015},}
@phdthesis{Bonacina-phdthesis,author={Bonacina, Ilario},doi={10.1007/978-3-319-73453-8},month=dec,school={Sapienza University of Rome},title={Space in weak propositional proof systems},year={2015},}
2014
Total Space in Resolution
Ilario
Bonacina
,
Nicola
Galesi
,
and
Neil
Thapen
In Proceedings of FOCS’14 (55th IEEE Symposium on Foundations of Computer Science) , Dec 2014
@inproceedings{BGT14-focs,author={Bonacina, Ilario and Galesi, Nicola and Thapen, Neil},title={Total Space in Resolution},booktitle={FOCS'14 (55th IEEE Symposium on Foundations of Computer Science)},doi={10.1109/FOCS.2014.74},pages={641--650},volume={38},year={2014},}
Proofs of Space: When Space Is of the Essence
Giuseppe
Ateniese
,
Ilario
Bonacina
,
Antonio
Faonio
, and
1 more author
In Proceedings of SCN’14 (9th International Conference on Security and Cryptography for Networks) , Dec 2014
@inproceedings{ABFG14-scn,author={Ateniese, Giuseppe and Bonacina, Ilario and Faonio, Antonio and Galesi, Nicola},booktitle={SCN'14 (9th International Conference on Security and Cryptography for Networks)},doi={10.1007/978-3-319-10879-7_31},pages={538--557},title={Proofs of Space: When Space Is of the Essence},year={2014},}
2013
Pseudo-partitions, transversality and locality: A Combinatorial Characterization for the Space Measure in Algebraic Proof Systems
Ilario
Bonacina
,
and
Nicola
Galesi
In Proceedings of ITCS’13 (4th Conference on Innovations in Theoretical Computer Science) , Dec 2013
@inproceedings{BG13-itcs,author={Bonacina, Ilario and Galesi, Nicola},booktitle={ITCS'13 (4th Conference on Innovations in Theoretical Computer Science)},doi={10.1145/2422436.2422486},pages={455--472},title={Pseudo-partitions, transversality and locality: A Combinatorial Characterization for the Space Measure in Algebraic Proof Systems},year={2013},}
