4 papers
Semi-Algebraic Proof Systems for QBF
Olaf Beyersdorff, Ilario Bonacina, Kaspar Kasche +2
We introduce new semi-algebraic proof systems for Quantified Boolean Formulas (QBF) analogous to the propositional systems Nullstellensatz, Sherali-Adams and Sum-of-Squares. We tra…
Redundancy rules for MaxSAT
Ilario Bonacina, Maria Luisa Bonet, Sam Buss +1
The concept of redundancy in SAT leads to more expressive and powerful proof search techniques, e.g., able to express various inprocessing techniques, and originates interesting hi…
Clique Is Hard on Average for Regular Resolution
Albert Atserias, Ilario Bonacina, Susanna F. de Rezende +3
We prove that for regular resolution requires length to establish that an Erdős-Rényi graph with appropriately chosen edge density does not contain a…
Space proof complexity for random 3-CNFs
Patrick Bennett, Ilario Bonacina, Nicola Galesi +3
We investigate the space complexity of refuting -CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random -CNF…