Computable Short Proofs

摘要

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 [1] or Frege systems [2]-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. Moreover, we introduce 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.