The complexity of variable minimal formulas

被引：2

作者：

Chen ZhenYu ^{[1
,2
]}

Xu BaoWen ^{[1
]}

Ding DeCheng ^{[3
]}

机构：

[1] Nanjing Univ, Natl Key Lab Novel Software Technol, Nanjing 210093, Peoples R China

[2] Nanjing Univ, Software Inst, Nanjing 210093, Peoples R China

[3] Nanjing Univ, Dept Math, Nanjing 210093, Peoples R China

来源：

CHINESE SCIENCE BULLETIN | 2010年 / 55卷 / 18期

基金：

国家高技术研究发展计划(863计划); 中国国家自然科学基金;

关键词：

minimal unsatisfiability; prime implication; variable minimal equivalence; variable minimal satisfiability; FACETS;

D O I：

10.1007/s11434-010-3127-2

中图分类号：

O [数理科学和化学]; P [天文学、地球科学]; Q [生物科学]; N [自然科学总论];

学科分类号：

07 ; 0710 ; 09 ;

摘要：

Based on the common properties of logic formulas: equivalence and satisfiability, the concept of variable minimal formulas with property preservation is introduced. A formula is variable minimal if the resulting sub-formulas with any variable omission will change the given property. Some theoretical results of two classes: variable minimal equivalence (VME) and variable minimal satisfiability (VMS) are studied. We prove that VME is NP-complete, and VMS is in D-P and coNP-hard.

引用

页码：1957 / 1960

页数：4

共 19 条

[1] Applying variable minimal unsatisfiability in model checking [J].

Chen, Zhen-Yu ;

Tao, Zhi-Hong ;

Kleine, Büning Hans ;

Wang, Li-Fu .

Ruan Jian Xue Bao/Journal of Software, 2008, 19 (01) :39-47

[2]

Chen Z, 2006, LECT NOTES COMPUT SC, V3959, P262

[3]

CHEN ZY, 2007, LNCS, V4767, P363

[4]

CHEN ZY, 2008, 23 ANN ACM S APPL CO, P390

[5]

CHILENSKI JJ, 1994, SOFTWARE ENG J, V9, P200

[6]

Cook S., 1971, STOC '71: Proceedings of the third annual ACM symposium on Theory of computing, P151

[7]

Kleine BuningH., 1999, Propositional Logic

[8] An extended fault class hierarchy for specification-based testing [J].

Lau, MF ;

Yu, YT .

ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2005, 14 (03) :247-276

[9] Formal verification techniques based on Boolean satisfiability problem [J].

Li, XW ;

Li, GH ;

Shao, M .

JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2005, 20 (01) :38-47

[10] THE COMPLEXITY OF FACETS RESOLVED [J].

PAPADIMITRIOU, CH ;

WOLFE, D .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1988, 37 (01) :2-13

← 1 2 →