Complexity of finding short resolution proofs

DOI10.1007/BFB0029974MaRDI QIDQ4699307zbMATH OpenFDO

Authors Kazuo Iwama

Publication date 1 February 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0029974

zbMATH Keywords

finding a shortest resolution proof for a CNF formulasatisfiability

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Minimum propositional proof length is NP-hard to linearly approximate (extended abstract)
• Automating resolution is NP-hard
• Minimum propositional proof length is NP-hard to linearly approximate
• On the complexity and inapproximability of shortest implicant problems
• scientific article; zbMATH DE number 1955763

Cited in

(22)

• Finding a tree structure in a resolution proof is NP-complete
• Pool resolution is NP-hard to recognize
• Transformation rules for CNOT-based quantum circuits and their applications
• Computational aspects of infeasibility analysis in mixed integer programming
• Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas
• Andrews Skolemization may shorten resolution proofs non-elementarily
• Polynomial time algorithms for optimal length tree-like refutations of linear infeasibility in UTVPI constraints
• Copy complexity of Horn formulas with respect to unit read-once resolution
• A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints
• NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability
• Minimum propositional proof length is NP-hard to linearly approximate (extended abstract)
• scientific article; zbMATH DE number 1955763 (Why is no real title available?)
• Are Short Proofs Narrow? QBF Resolution is not Simple.
• Are Short Proofs Narrow? QBF Resolution Is Not So Simple
• On the complexity and inapproximability of shortest implicant problems
• Finding the hardest formulas for resolution
• Quantum automating TC^0-Frege is LWE-hard
• Quantum automating \(\mathrm{TC}^0\)-Frege is LWE-hard
• On the automatability of tree-like k-DNF resolution
• On finding short resolution refutations and small unsatisfiable subsets
• Density condensation of Boolean formulas
• The NP-hardness of finding a directed acyclic graph for regular resolution

This page was built for publication: Complexity of finding short resolution proofs

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