Abstract
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.
In this talk, we discuss some recently proposed strong proof systems that are more suitable for mechanization. These proof systems are 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 these proof systems on two famous problems: the pigeon hole principle and mutilated chessboards. For both problems, we present proofs of linear size without new variables. Finally, we describe initial methods to find such proofs automatically.