Davis-Putnam resolution versus unrestricted resolution
From MaRDI portal
Publication:1353991
DOI10.1007/BF01531027zbMath0865.03010MaRDI QIDQ1353991
Publication date: 13 May 1997
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Davis-Putnam resolution; proofs of superpolynomial length; unrestricted resolution proofs; unsatisfiable propositional formulas
Related Items
On Exponential Lower Bounds for Partially Ordered Resolution, Reflections on Proof Complexity and Counting Principles, The complexity of resolution refinements, Resolution and binary decision diagrams cannot simulate each other polynomially, Expansion-based QBF solving versus Q-resolution, On Q-Resolution and CDCL QBF Solving
Cites Work
- Unnamed Item
- Resolution proofs of generalized pigeonhole principles
- The intractability of resolution
- Unrestricted resolution versus N-resolution
- On the complexity of regular resolution and the Davis-Putnam procedure
- Many hard examples for resolution
- Hard examples for resolution
- The relative efficiency of propositional proof systems
- A Computing Procedure for Quantification Theory