Many hard examples for resolution
- 1 October 1988
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 35 (4) , 759-768
- https://doi.org/10.1145/48014.48016
Abstract
For every choice of positive integers c and k such that k ≥ 3 and c 2 - k ≥ 0.7, there is a positive number ε such that, with probability tending to 1 as n tends to ∞, a randomly chosen family of cn clauses of size k over n variables is unsatisfiable, but every resolution proof of its unsatisfiability must generate at least (1 + ε) n clauses.Keywords
This publication has 12 references indexed in Scilit:
- Hard examples for resolutionJournal of the ACM, 1987
- The intractability of resolutionTheoretical Computer Science, 1985
- On the complexity of regular resolution and the Davis-Putnam procedureTheoretical Computer Science, 1977
- Some applications of a theorem of RadoMathematika, 1968
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960
- A THEOREM ON INDEPENDENCE RELATIONSThe Quarterly Journal of Mathematics, 1942
- On Representatives of SubsetsJournal of the London Mathematical Society, 1935
- Über Transformationen im GebietekalkülMathematische Annalen, 1913
- Über die Auflösung von Gleichungen im logischen GebietekalkulMathematische Annalen, 1910