Minimum propositional proof length is NP-Hard to linearly approximate

Journal of Symbolic Logic 66 (1):171-191 (2001)
  Copy   BIBTEX

Abstract

We prove that the problem of determining the minimum propositional proof length is NP- hard to approximate within a factor of 2 log 1 - o(1) n . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 76,101

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2009-01-28

Downloads
226 (#55,583)

6 months
1 (#447,139)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Towards NP – P via proof complexity and search.Samuel R. Buss - 2012 - Annals of Pure and Applied Logic 163 (7):906-917.

Add more citations

References found in this work

Some remarks on lengths of propositional proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.

Add more references