The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

Skip to content



Separations between propositional proof systems related to clause learning

Johannsen, J (Ludwig-Maximilians-Universität München)
Wednesday 28 March 2012, 10:00-10:30

Seminar Room 1, Newton Institute


Resolution trees with lemmas (RTL) are a resolution-based propositional proof system that is related to the DLL algorithm with clause learning, with its fragments RTL(k) being 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 between the proof systems RTL(k) and RTL(k+1) is shown, indicating that a minimal increase in the width of learned clauses can lead to an exponential speed-up for clause learning algorithms.


The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.

Back to top ∧