Many hard examples for resolution

ABSTRACT

For every choice of positive integers c and k such that k ≥ 3 and c2-k ≥ 0.7, there is a positive number &egr; 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 + &egr;)n clauses.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	BIBEL, W. Automated Theorem Proving, 2nd ed. Vieweg, Braunschweig, 1987.
	2	BLAKE, A. Canonical Expressions in Boolean algebra. Ph.D. dissertation. Univ. of Chicago, Chicago, Ill., 1937.
	3	CHV,~TAL, V. Probabilistic methods in graph theory. Ann. Oper. Res. 1 (1984), 17 l- 182.
	4	Stephen A. Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing, p.151-158, May 03-05, 1971, Shaker Heights, Ohio, United States [doi>10.1145/800157.805047]
	5	Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
	6	GALIL, Z. On the complexity of regular resolution and the Davis-Putnam procedure. Theoret. Comput. Sci. 4 (1977), 23-46.
	7	HAKEN, A. The intractability of resolution. Theoret. Comput. Sci. 39 (i 985), 297-308.
	8	HALL, P. On representatives of subsets. Jr. London Math. Soc. I0 (1935), 26-30.
	9	HAMMER (IVANESCU), P. L., AND RUDEANU, S. Boolean Methods in Operations Research and Related Areas. Springer-Verlag, Berlin, Heidelberg, New York, 1968.
	10	HOFFMAN, A. J., AND KUHN, H.W. On systems of distinct representatives. In Linear Inequalities and Related Systems. Annals of Mathematical Studies, vol. 38. Princeton University Press, Princeton, N.J., 1956, pp. 199-206.
	11	LOWENHEIM, L. l~lber das Aufl6sungsproblem im logischen Klassenkalkul. Sitzungsber. Berlin Math. Ges. 7 (1908), 89-94.
	12	Lt)WENHEIM, L. Ober die Aufl6sung von Gleichungen im logischen Gebietkalkul. Math. Ann. 68 ( 1910), 169-207.
	13	LOWENHEIM, L. 13ber Transformationen im Gebietkalkul. Math. Ann. 73 (1913), 245-272.
	14	RADO, R. A theorem on independence relations. Quart. J. Math. (Oxford) 13 (1942), 83-89.
	15	J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
	16	TSEITIN, G. S. Oil the complexity of derivations in the propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part 2. Consultants Bureau, New York- London, 1968, pp. I 15-125.
	17	Alasdair Urquhart, Hard examples for resolution, Journal of the ACM (JACM), v.34 n.1, p.209-219, Jan. 1987 [doi>10.1145/7531.8928]
	18	WELSH, D. J.A. Some applications of a theorem ofRado. Mathematika 15 (1968), 199-203.