Browsing by Author "Lauria, Massimo"
Now showing items 19 of 9

Circular (yet sound) proofs
Atserias, Albert; Lauria, Massimo (Springer, 2019)
Conference report
Open AccessWe introduce a new way of composing proofs in rulebased proof systems that generalizes treelike and daglike proofs. In the new definition, proofs are directed graphs of derived formulas, in which cycles are allowed as ... 
Circular (yet sound) proofs in propositional logic
Atserias, Albert; Lauria, Massimo (Association for Computing Machinery (ACM), 202307)
Article
Open AccessProofs in propositional logic are typically presented as trees of derived formulas or, alternatively, as directed acyclic graphs of derived formulas. This distinction between treelike vs. daglike structure is particularly ... 
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 kclique. 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), 202108)
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 kclique. This lower bound is optimal up to the multiplicative ... 
Narrow proofs may be maximally long
Atserias, Albert; Lauria, Massimo; Nordström, Jakob (20160703)
Article
Open AccessWe prove that there are 3CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n(Omega(w)). This shows that the simple counting argument that any formula refutable ... 
Narrow proofs may be maximally long
Atserias, Albert; Lauria, Massimo; Nordström, Jakob (Institute of Electrical and Electronics Engineers (IEEE), 2014)
Conference report
Open AccessWe prove that there are 3CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n¿(w). This shows that the simple counting argument that any formula refutable in ... 
On vanishing sums of roots of unity in polynomial calculus and sumofsquares
Bonacina, Ilario; Galesi, Nicola; Lauria, Massimo (Schloss Dagstuhl  LeibnizZentrum 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 sumofsquares
Bonacina, Ilario; Galesi, Nicola; Lauria, Massimo (202312)
Article
Open AccessWe introduce a novel take on sumofsquares 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 ... 
Tradeoffs between time and memory in a tighter model of CDCL SAT solvers
Elffers, J.; Johannsen, Jan; Lauria, Massimo; Magnard, Thomas; Nordström, Jakob; Vinyals, Marc (2016)
Conference report
Open AccessA long line of research has studied the power of conflict driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially ...