Minimum propositional proof length is NP-hard to linearly approximate

DOI10.2307/2694916zbMATH Open0977.03032OpenAlexW2006906201MaRDI QIDQ2732273FDOQ2732273

Authors: Michael Alekhnovich, Shlomo Moran, Toniann Pitassi, Samuel R. Buss 

Publication date: 21 January 2002

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2694916

Recommendations

• scientific article; zbMATH DE number 1222561
• Theory and Applications of Satisfiability Testing
• Lower bounds to the size of constant-depth propositional proofs
• Proof mining in \(L_{1}\)-approximation
• Some remarks on lengths of propositional proofs
• Simplified lower bounds for propositional proofs
• Propositional proofs and reductions between NP search problems
• scientific article; zbMATH DE number 1342249
• scientific article; zbMATH DE number 1860672
• The Complexity of Propositional Proofs

zbMATH Keywords

lower boundsresolutionhardness of approximationsequent calculusFrege systemspolynomial calculusresolution refutationsminimum propositional proof length

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)

Cites Work

• Approximation algorithms for NP-hard problems.
• The relative efficiency of propositional proof systems
• On the hardness of approximating minimization problems
• The hardness of approximate optima in lattices, codes, and systems of linear equations
• Some remarks on lengths of propositional proofs

Cited In (14)

• On finding short resolution refutations and small unsatisfiable subsets
• On the hardness of approximating the min-hack problem
• Towards NP-P via proof complexity and search
• Approximation algorithms for the Label-Cover\(_{\text{MAX}}\) and Red-Blue Set Cover problems
• Special issue in memory of Misha Alekhnovich. Foreword
• Shortening of proof length is elusive for theorem provers
• An upper bound for resolution size: characterization of tractable SAT instances
• Finding a tree structure in a resolution proof is NP-complete
• On the automatizability of resolution and related propositional proof systems
• Short Proofs Are Hard to Find
• Pool resolution is NP-hard to recognize
• The NP-hardness of finding a directed acyclic graph for regular resolution
• NP-hardness of approximating meta-complexity: a cryptographic approach
• Cost-optimal planning, delete relaxation, approximability, and heuristics

This page was built for publication: Minimum propositional proof length is NP-hard to linearly approximate

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2732273)