Pool resolution is NP-hard to recognize

DOI10.1007/S00153-009-0152-4MaRDI QIDQ1042441zbMATH OpenOpenAlexFDO

Authors Samuel R. Buss

Publication date 14 December 2009

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial 4.0 International

Full work available at URL https://doi.org/10.1007/s00153-009-0152-4

zbMATH Keywords

NP-completenessresolutionproof search

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Complexity of proofs (03F20)

Recommendations

• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
• An improved separation of regular resolution from pool resolution and clause learning
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Automating resolution is NP-hard
• Small Stone in pool
• Improved separations of regular resolution from clause learning proof systems
• Extended resolution simulates binary decision diagrams
• Determinization of Resolution by an Algorithm Operating on Complete Assignments
• 2 -Way vs.d -Way Branching for CSP

Cites work

• scientific article; zbMATH DE number 1765669 (Why is no real title available?)
• scientific article; zbMATH DE number 1361489 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• Finding a tree structure in a resolution proof is NP-complete
• Minimum propositional proof length is NP-hard to linearly approximate
• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
• Resolution Is Not Automatizable Unless W[P] Is Tractable
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• The NP-hardness of finding a directed acyclic graph for regular resolution

Cited in

(5)

• Small Stone in pool
• The NP-hardness of finding a directed acyclic graph for regular resolution
• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
• Finding a tree structure in a resolution proof is NP-complete
• Automating resolution is NP-hard

This page was built for publication: Pool resolution is NP-hard to recognize

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