Abstract
We prove that the problem of determining the minimum propositional proof length is NP-hard to approximate within any constant factor. These results hold for all Frege systems, for all extended Frege systems, for resolution and Horn resolution, and for the sequent calculus and the cut-free sequent calculus. Also, if NP is not in \(QP = DTIME(n^{log^{O(1)} n} )\), then it is impossible to approximate minimum propositional proof length within a factor of \(2^{log^{(1 - \varepsilon )} n}\) for any є > 0. All these hardness of approximation results 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 prove the same hardness results for Monotone Minimum (Circuit) Satisfying Assignment.
Supported in part by INTAS grant N96-753
Supported in part by NSF grant DMS-9503247 and grant INT-9600919/ME-103 from NSF and MšMT (Czech Republic)
Research supported by the Bernard Elkin Chair for Computer Science and by US-Israel grant 95-00238
Supported in part by NSF grant CCR-9457782, US-Israel BSF grant 95-00238, and grant INT-9600919/ME-103 from NSF and MSMT (Czech Republic)
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. Arora, L. Babai, J. Stern, and Z. Sweedyk, The hardness of approximate optima in lattices, codes, and systems of linear equations, Journal of Computer and System Sciences, 54 (1997), pp. 317–331. Earlier version in Proc. 34th Symp. Found. of Comp. Sci., 1993, pp.724–733.
S. Arora and C. Lund, Hardness of approximations, in Approximation Algorithms for NP-hard Problems, D. S. Hochbaum, ed., PWS Publishing Co., Boston, 1996, p. ???
P. Beame and T. Pitassi, Simplified and improved resolution lower bounds, in Proceedings, 37th Annual Symposium on Foundations of Computer Science, Los Alamitos, California, 1996, IEEE Computer Society, pp. 274–282.
M. Bellare, Proof checking and approximation: Towards tight results, SIGACT News, 27 (1996), pp. 2–13. Revised version at http://www-cse.ucsd.edu/users/mihir.
M. Bellare, S. Goldwasser, C. Lund, and A. Russell, Efficient probabalistically checkable proofs and applications to approximation, in Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, Association for Computing Machinery, 1993, pp. 294–304.
M. L. Bonet, T. Pitassi, and R. Raz, No feasible interpolation for TC0-Frege proofs, in Proceedings of the 38th Annual Symposium on Foundations of Computer Science, Piscataway, New Jersey, 1997, IEEE Computer Society, pp. 264–263.
S. R. Buss, On Gödel's theorems on lengths of proofs II: Lower bounds for recognizing k symbol provability, in Feasible Mathematics II, P. Clote and J. Remmel, eds., Birkhäauser-Boston, 1995, pp. 57–90.
M. Clegg, J. Edmonds, and R. Impagliazzo, Using the Groebner basis algorithm to find proofs of unsatisfiability, in Proceedings of the Twenty-eighth Annual ACM Symposium on the Theory of Computing, Association for Computing Machinery, 1996, pp. 174–183.
U. Feige, A threshold of ln n for approximating set cover, in Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, Association for Computing Machinery, 1996, pp. 314–318.
K. Iwama, Complexity of finding short resolution proofs, in Mathematical Foundations of Computer Science 1997, I. Prívara and P. Ruzicka, eds., Lecture Notes in Computer Science #1295, Springer-Verlag, 1997, pp. 309–318.
K. Iwama and E. Miyano, Intractibility of read-once resolution, in Proceedings of the Tenth Annual Conference on Structure in Complexity Theory, Los Alamitos, California, 1995, IEEE Computer Society, pp. 29–36.
S. Khanna, M. Sudan, and L. Trevisan, Constraint satisfaction: The approximability of minimization problems, in Twelfth Annual Conference on Computational Complexity, IEEE Computer Society, 1997, pp. 282–296.
J. Krajíček and P. Pudlák, Some consequences of cryptographic conjectures for S 12 and EF, in Logic and Computational Complexity, D. Leivant, ed., Berlin, 1995, Springer-Verlag, pp. 210–220.
C. Lund and M. Yannakakis, On the hardness of approximating minimization problems, Journal of the Association for Computing Machinery, 41 (1994), pp. 960–981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alekhnovich, M., Buss, S., Moran, S., Pitassi, T. (1998). Minimum propositional proof length is NP-hard to linearly approximate. In: Brim, L., Gruska, J., Zlatuška, J. (eds) Mathematical Foundations of Computer Science 1998. MFCS 1998. Lecture Notes in Computer Science, vol 1450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055766
Download citation
DOI: https://doi.org/10.1007/BFb0055766
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64827-7
Online ISBN: 978-3-540-68532-6
eBook Packages: Springer Book Archive