79 citations · 93 across the 20 of their papers we have counts for
Showing 2014Show all
2 papers · 1 filter
cs.CC2014★ 3 cited
Narrow Proofs May Be Maximally Long
Albert Atserias, Massimo Lauria, Jakob Nordström
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 co…
cs.LO2014★ 79 cited
Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
Albert Atserias, Johannes Klaus Fichte, Marc Thurley
We offer a new understanding of some aspects of practical SAT-solvers that are based on DPLL with unit-clause propagation, clause-learning, and restarts. We do so by analyzing a co…