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 Citations and Data
Attribution-NonCommercial-NoDerivatives 4.0 International