Equivalence models for quantified Boolean formulas

被引：0

作者：

Büning, HK

Zhao, XS

机构：

[1] Sun Yat Sen Univ, Inst Log & Cognit, Guangzhou 510275, Peoples R China

[2] Univ Paderborn, Dept Comp Sci, D-33095 Paderborn, Germany

来源：

THEORY AND APPLICATIONS OF SATISFIABILITY TESTING | 2005年 / 3542卷

关键词：

quantified Boolean formula; equivalence model; model checking; complexity; equivalence; satisfiability;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In this paper, the notion of equivalence models for quantified Boolean formulas with free variables is introduced. The computational complexity of the equivalence model checking problem is investigated in the general case and in some restricted cases. We also establish a connection between the structure of some quantified Boolean formulas and the structure of models.

引用

页码：224 / 234

页数：11

共 15 条

[1]

[Anonymous], 1979, Computers and Intractablity: A Guide to the Theoryof NP-Completeness

[2] LINEAR-TIME ALGORITHM FOR TESTING THE TRUTH OF CERTAIN QUANTIFIED BOOLEAN FORMULAS [J].

ASPVALL, B ;

PLASS, MF ;

TARJAN, RE .

INFORMATION PROCESSING LETTERS, 1979, 8 (03) :121-123

[3]

Buning Hans Kleine, 1999, Cambridge Tracts in Theoretical Computer Science, V48

[4]

Büning HK, 2004, LECT NOTES COMPUT SC, V2919, P93

[5] RESOLUTION FOR QUANTIFIED BOOLEAN-FORMULAS [J].

BUNING, HK ;

KARPINSKI, M ;

FLOGEL, A .

INFORMATION AND COMPUTATION, 1995, 117 (01) :12-18

[6]

BUNING HK, 2004, IN PRESS LNCS

[7]

CADOLI M, 2000, HIGHLIGHTS SATISFIAB

[8]

Cook S. A., 1999, B SECTION LOGIC, V28, P119, DOI 10.1.1.150.2814.

[9]

GIUNCHIGLIA E, 2001, P IJCAR SIEN

[10]

LETZ R, 2001, P IJCAR SIEN

← 1 2 →