Open Collections

Computable Short Proofs

Banff International Research Station for Mathematical Innovation and Discovery

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.

Mathematics; Computer science; Mathematical logic and foundations; Theoretical computer science

video/mp4

Author affiliation: University of Texas at Austin

2019-03-30

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/69357

Unreviewed

http://creativecommons.org/licenses/by-nc-nd/4.0/