Now showing items 1-4 of 4

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