An algorithm for the class of pure implicational formulas

被引：8

作者：

Franco, J

Goldsmith, J

Schlipf, J

Speckenmeyer, E ^{[1
]}

Swaminathan, RP

机构：

[1] Univ Cincinnati, ECECS, Cincinnati, OH 45221 USA

[2] Univ Kentucky, Dept Comp Sci, Lexington, KY 40506 USA

[3] Univ Cologne, Inst Informat, D-5000 Cologne 41, Germany

[4] Lucent Technol, Bell Labs, Murray Hill, NJ 07974 USA

来源：

DISCRETE APPLIED MATHEMATICS | 1999年 / 97卷

关键词：

satisfiability; implicational formulas; fixed parameter tractable; Boolean functions;

D O I：

10.1016/S0166-218X(99)00038-4

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

Heusch introduced the notion of pure implicational formulas. He showed that the falsifiability problem for pure implicational formulas with k negations is solvable in time O(n(k)). Such falsifiability results are easily transformed to satisfiability results on CNF formulas. We show that the falsifiability problem for pure implicational formulas is solvable in time O(k(k)n(2)), which is polynomial for a fixed k. Thus this problem is fixed-parameter tractable. (C) 1999 Elsevier Science B.V. All rights reserved.

引用

页码：89 / 106

页数：18

共 9 条

[1]

[Anonymous], 1992, C NUMERANTIUM

[2] ON GENERALIZED HORN FORMULAS AND K-RESOLUTION [J].

BUNING, HK .

THEORETICAL COMPUTER SCIENCE, 1993, 116 (02) :405-413

[3]

Cook S.A., 1971, P 3 ANN ACM S THEOR, P151, DOI DOI 10.1145/800157.805047

[4]

Coppersmith D., 1981, 22 ANN S FDN COMPUTE, P82

[5] A HIERARCHY OF TRACTABLE SATISFIABILITY PROBLEMS [J].

DALAL, M ;

ETHERINGTON, DW .

INFORMATION PROCESSING LETTERS, 1992, 44 (04) :173-180

[6] POLYNOMIALLY SOLVABLE SATISFIABILITY PROBLEMS [J].

GALLO, G ;

SCUTELLA, MG .

INFORMATION PROCESSING LETTERS, 1988, 29 (05) :221-227

[7]

HEUSCH P, 1995, LECT NOTES COMPUTER, V969, P221

[8]

Nesetril J., 1985, COMM MATH U CAROL, V26, P415

[9]

TREUMPER K, 1998, EFFECTIVE LOGIC COMP

← 1 →