Resolution trees with lemmas ($\mathrm{RTL}$) are a resolution-based propositional proof system that is related to the DPLL algorithm with clause learning. Its fragments $\mathrm{RTL}(k)$ are related to clause learning algorithms where the width of learned clauses is bounded by $k$.

For every $k$ up to $O(\log n)$, an exponential separation ... more >>>

It has been observed empirically that clause learning does not significantly improve the performance of a SAT solver when restricted
to learning clauses of small width only. This experience is supported by lower bound theorems. It is shown that lower bounds on the runtime of width-restricted clause learning follow from ... more >>>

This paper gives two distinct proofs of an exponential separation
between regular resolution and unrestricted resolution.
The previous best known separation between these systems was
quasi-polynomial.

more >>>

We prove an exponential lower bound for tree-like Cutting Planes
refutations of a set of clauses which has polynomial size resolution
refutations. This implies an exponential separation between tree-like
and dag-like proofs for both Cutting Planes and resolution; in both
cases only superpolynomial separations were known before.
In order to ... more >>>

Using a notion of real communication complexity recently
introduced by J. Krajicek, we prove a lower bound on the depth of
monotone real circuits and the size of monotone real formulas for
st-connectivity. This implies a super-polynomial speed-up of dag-like
over tree-like Cutting Planes proofs.

more >>>