On a generalization of extended resolution

被引：70

作者：

Kullmann, O ^{[1
]}

机构：

[1] Univ Frankfurt, Fachbereich Math, D-60054 Frankfurt, Germany

来源：

DISCRETE APPLIED MATHEMATICS | 1999年 / 97卷

关键词：

propositional logic; extended resolution; blocked clauses; generalized extended resolution; lower bounds;

D O I：

10.1016/S0166-218X(99)00037-2

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

Motivated by improved SAT algorithms ((O. Kullmann, DIMACS Series, vol. 35, Amer. Math. Sec., Providence, RI, 1997; O. Kullmann, Theoret. Comput. Sci. (1999); 0. Kullmann, Inform. Comput., submitted); yielding new worst-case upper bounds) a natural parameterized generalization GER of Extended Resolution (ER) is introduced. ER can simulate polynomially GER, but GER allows special cases for which exponential lower bounds can be proven. (C) 1999 Elsevier Science B.V. All rights reserved.

引用

页码：149 / 176

页数：28

共 22 条

[1] Simplified and improved resolution lower bounds [J].

Beame, P ;

Pitassi, T .

37TH ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS, 1996, :274-282

[2] A FEASIBLY CONSTRUCTIVE LOWER BOUND FOR RESOLUTION PROOFS [J].

COOK, S ;

PITASSI, T .

INFORMATION PROCESSING LETTERS, 1990, 34 (02) :81-85

[3]

Cook S.A., 1974, 6 ANN ACM S THEOR CO, P135

[4] RELATIVE EFFICIENCY OF PROPOSITIONAL PROOF SYSTEMS [J].

COOK, SA ;

RECKHOW, RA .

JOURNAL OF SYMBOLIC LOGIC, 1979, 44 (01) :36-50

[5]

COOK SA, 1976, SIGACT NEWS OCT, P28

[6]

Cook Stephen A, 1974, SIGACT NEWS, V6, P15, DOI [10.1145/1008311.1008313, DOI 10.1145/1008311.1008313]

[7]

FRANCO J, 1996, WORKSH SAT PROBL

[8] THE INTRACTABILITY OF RESOLUTION [J].

HAKEN, A .

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

[9] PROPOSITIONAL PROOF SYSTEMS, THE CONSISTENCY OF 1ST ORDER THEORIES AND THE COMPLEXITY OF COMPUTATIONS [J].

KRAJICEK, J ;

PUDLAK, P .

JOURNAL OF SYMBOLIC LOGIC, 1989, 54 (03) :1063-1079

[10]

KULLMANN O, 1996, EXPONENTIAL LOWER BO

← 1 2 3 →