MANY HARD EXAMPLES FOR RESOLUTION

被引：240

作者：

CHVATAL, V ^{[1
]}

SZEMEREDI, E ^{[1
]}

机构：

[1] HUNGARIAN ACAD SCI,INST MATH,H-1361 BUDAPEST 5,HUNGARY

来源：

JOURNAL OF THE ACM | 1988年 / 35卷 / 04期

关键词：

Mathematical Techniques - Graph Theory - Probability - Random Processes;

D O I：

10.1145/48014.48016

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

It is proved that for every choice of positive integers c and k such that k ≥ 3 and c2-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. The proof makes use of random hypergraphs.

引用

页码：759 / 768

页数：10

共 18 条

[1]

[Anonymous], 1971, STOC 71, DOI DOI 10.1145/800157.805047

[2]

Bibel W., 1987, AUTOMATED THEOREM PR, V2nd

[3]

BLAKE A, 1937, THESIS U CHICAGO CHI

[4]

Chvatal V., 1984, Annals of Operations Research, V1, P171, DOI 10.1007/BF01874387

[5] A COMPUTING PROCEDURE FOR QUANTIFICATION THEORY [J].

DAVIS, M ;

PUTNAM, H .

JOURNAL OF THE ACM, 1960, 7 (03) :201-215

[6]

Galil Z., 1977, Theoretical Computer Science, V4, P23, DOI 10.1016/0304-3975(77)90054-8

[7] THE INTRACTABILITY OF RESOLUTION [J].

HAKEN, A .

THEORETICAL COMPUTER SCIENCE, 1985, 39 (2-3) :297-308

[8]

Hall P., 1935, J LONDON MATH SOC, V1, P26, DOI [10.1112/jlms/s1-10.37.26, DOI 10.1112/JLMS/S1-10.37.26]

[9]

HOFFMAN AJ, 1956, ANN MATH STUD, V38, P199

[10] Transformations in calculus. [J].

Lowenheim, L .

MATHEMATISCHE ANNALEN, 1913, 73 :245-272

← 1 2 →