Journal article:
Misha Alekhnovich, Samuel R. Buss, Shlomo Moran, and Toniann
Pitassi.
"Minimum Propositional Proof Length is NP-Hard to Linearly
Approximate."
Journal of Symbolic Logic 66 (2001) 171-191.
Download journal article version: postscript or PDF.
Conference proceedings (earlier version).
Misha Alekhnovich, Samuel R. Buss, Shlomo Moran, and Toniann
Pitassi.
"Minimum Propositional Proof Length is NP-Hard to Linearly
Approximate (Extended Abstract)."
Proceedings, Mathematical Foundations of Computer Science (MFCS'98)
Lecture Notes in Computer Science #1450,
Springer-Verlag, 1998, pp. 176-184.
Download conference proceedings extended abstract: postscript or PDF.
Journal version abstract: We prove that the problem of determining the minimum propositional proof length is NP-hard to approximate within a factor of \factor. 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.