Browsing by Author "Bonacina, Ilario"
Now showing items 1-8 of 8
-
Clique is hard on average for regular resolution
Atserias, Albert; Bonacina, Ilario; Rezende, Susanna F. de; Lauria, Massimo; Nordström, Jakob; Razborov, Alexander (Association for Computing Machinery (ACM), 2018)
Conference report
Open AccessWe prove that for k ≪4√n regular resolution requires length nΩ(k) to establish that an Erdős–Rényi graph with appropriately chosen edge density does not contain a k-clique. This lower bound is optimal up to the multiplicative ... -
Clique is hard on average for regular resolution
Atserias, Albert; Bonacina, Ilario; De Rezende, Susanna F.; Lauria, Massimo; Nordström, Jakob; Razborov, Alexander (Association for Computing Machinery (ACM), 2021-08)
Article
Open AccessWe prove that for k ≪ 4√n regular resolution requires length nΩ(k) to establish that an Erdős–Rényi graph with appropriately chosen edge density does not contain a k-clique. This lower bound is optimal up to the multiplicative ... -
Frege systems for quantified Boolean logic
Beyersdorffm, Olaf; Bonacina, Ilario; Chew, Leroy; Pich, Ján (2020-05-09)
Article
Open AccessWe 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 ... -
On vanishing sums of roots of unity in polynomial calculus and sum-of-squares
Bonacina, Ilario; Galesi, Nicola; Lauria, Massimo (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022)
Conference report
Open AccessVanishing 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 ... -
On vanishing sums of roots of unity in polynomial calculus and sum-of-squares
Bonacina, Ilario; Galesi, Nicola; Lauria, Massimo (2023-12)
Article
Open AccessWe 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 ... -
Polynomial calculus for MaxSAT
Bonacina, Ilario; Bonet Carbonell, M. Luisa; Levy Díaz, Jordi (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023)
Conference report
Open AccessMaxSAT 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 ... -
Polynomial calculus for optimization
Bonacina, Ilario; Bonet Carbonell, M. Luisa; Levy Díaz, Jordi (2024-12)
Article
Open AccessMaxSAT 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 ... -
Weighted, circular and semi-algebraic proofs
Bonacina, Ilario; Bonet Carbonell, M. Luisa; Levy Díaz, Jordi (2024-02-11)
Article
Open AccessIn 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 ...