BIRS Workshop Lecture Videos

Banff International Research Station Logo

BIRS Workshop Lecture Videos

Computable Short Proofs Heule, Marijn


The success of satisfiability solving presents us with an interesting peculiarity: modern solvers can frequently handle gigantic formulas while failing miserably on supposedly easy problems. Their poor performance is typically caused by the weakness of their underlying proof systemâ resolution. To overcome this obstacle, we need solvers that are based on stronger proof systems. Unfortunately, existing strong proof systemsâ such as extended resolution or Frege systemsâ do not seem to lend themselves to mechanization.

We present a new proof system that not only generalizes strong existing proof systems but that is also well-suited for mechanization. The proof system is surprisingly strong, even without the introduction of new variablesâ a key feature of short proofs presented in the proof-complexity literature. We demonstrate the strength of the new proof system on the famous pigeon hole formulas by providing short proofs without new variables. Moreover, we introduce satisfaction-driven clause learning, a new decision procedure that exploits the strengths of our new proof system and can therefore yield exponential speed-ups compared to state-of-the-art solvers based on resolution.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivatives 4.0 International