Minimum propositional proof length is NP-hard to linearly approximate

DOI10.2307/2694916MaRDI QIDQ2732273zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

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
• An upper bound for resolution size: characterization of tractable SAT instances
• Shortening of proof length is elusive for theorem provers
• 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)