Minimum propositional proof length is NP-hard to linearly approximate

DOI10.2307/2694916zbMath0977.03032OpenAlexW2006906201MaRDI QIDQ2732273

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

Publication date: 21 January 2002

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

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

zbMATH Keywords

sequent calculuslower boundsresolutionpolynomial calculushardness of approximationFrege systemsresolution 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)

Related Items (13)

On finding short resolution refutations and small unsatisfiable subsets ⋮ On the automatizability of resolution and related propositional proof systems ⋮ Shortening of Proof Length is Elusive for Theorem Provers ⋮ Towards NP-P via proof complexity and search ⋮ Special issue in memory of Misha Alekhnovich. Foreword ⋮ An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances ⋮ The NP-hardness of finding a directed acyclic graph for regular resolution ⋮ Approximation algorithms for the Label-Cover\(_{\text{MAX}}\) and Red-Blue Set Cover problems ⋮ Cost-optimal Planning, Delete Relaxation, Approximability, and Heuristics ⋮ Finding a tree structure in a resolution proof is NP-complete ⋮ Short Proofs Are Hard to Find ⋮ Pool resolution is NP-hard to recognize ⋮ On the hardness of approximating the min-hack problem

Cites Work

• Unnamed Item
• The hardness of approximate optima in lattices, codes, and systems of linear equations
• Some remarks on lengths of propositional proofs
• The relative efficiency of propositional proof systems
• On the hardness of approximating minimization problems

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