Minimum propositional proof length is NP-Hard to linearly approximate
Journal of Symbolic Logic 66 (1):171-191 (2001)
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.DOI
10.2307/2694916
My notes
Similar books and articles
Quantified propositional logic and the number of lines of tree-like proofs.Alessandra Carbone - 2000 - Studia Logica 64 (3):315-321.
The deduction rule and linear and near-linear proof simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
Propositional proof systems, the consistency of first order theories and the complexity of computations.Jan Krajíček & Pavel Pudlák - 1989 - Journal of Symbolic Logic 54 (3):1063-1079.
Interpolation theorems, lower Bounds for proof systems, and independence results for bounded arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
Proving theorems of the second order Lambek calculus in polynomial time.Erik Aarts - 1994 - Studia Logica 53 (3):373 - 387.
Bounded Arithmetic, Propositional Logic and Complexity Theory.Jan Krajíček - 1995 - Cambridge University Press.
Polynomial size proofs of the propositional pigeonhole principle.Samuel R. Buss - 1987 - Journal of Symbolic Logic 52 (4):916-927.
Review: Michael Alekhnovich, Sam Buss, Shlomo Moran, Toniann Pitassi, Minimum Propositional Proof Length Is NP-Hard to Linearly Approximate. [REVIEW]Alexander Razborov - 2002 - Bulletin of Symbolic Logic 8 (2):301-302.
Analytics
Added to PP
2009-01-28
Downloads
226 (#55,583)
6 months
1 (#447,139)
2009-01-28
Downloads
226 (#55,583)
6 months
1 (#447,139)
Historical graph of 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.
References found in this work
Some remarks on lengths of propositional proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.