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
DAVIS, M
PUTNAM, H
[J]. 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
HAKEN, A
[J]. 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.
Lowenheim, L
[J]. MATHEMATISCHE ANNALEN, 1913, 73 : 245 - 272

← 1 2 →