Now showing items 1-5 of 5

  • Circular (yet sound) proofs 

    Atserias, Albert; Lauria, Massimo (Springer, 2019)
    Conference report
    Open Access
    We introduce a new way of composing proofs in rule-based proof systems that generalizes tree-like and dag-like 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 Access
    We 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 ...
  • Narrow proofs may be maximally long 

    Atserias, Albert; Lauria, Massimo; Nordström, Jakob (Institute of Electrical and Electronics Engineers (IEEE), 2014)
    Conference report
    Open Access
    We prove that there are 3-CNF 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 ...
  • Narrow proofs may be maximally long 

    Atserias, Albert; Lauria, Massimo; Nordström, Jakob (2016-07-03)
    Article
    Open Access
    We prove that there are 3-CNF 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 ...
  • Trade-offs 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 Access
    A 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 ...