Browsing by Author "Lauria, Massimo"
Now showing items 15 of 5

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