Boolean functions as models for quantified Boolean formulas

被引:13
作者
Buening, Hans Kleine [1 ]
Subramani, K.
Zhao, Xishun
机构
[1] Univ Paderborn, Dept Comp Sci, D-33095 Paderborn, Germany
[2] W Virginia Univ, LDCSEE, Morgantown, WV 26506 USA
[3] Sun Yat Sen Univ, Inst Log & Cognit, Guangzhou 510275, Guangdong, Peoples R China
基金
中国国家自然科学基金;
关键词
quantified Boolean formula; Boolean function; model; complexity; satisfiability; propositional logic;
D O I
10.1007/s10817-007-9067-0
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
In this paper, we introduce the notion of models for quantified Boolean formulas. For various classes of quantified Boolean formulas and various classes of Boolean functions, we investigate the problem of determining whether a model exists. Furthermore, we show for these classes the complexity of the model checking problem, which is to check whether a given set of Boolean functions is a model for a formula. For classes of Boolean functions, we establish some characterizations in terms of classes of quantified Boolean formulas that have such a model.
引用
收藏
页码:49 / 75
页数:27
相关论文
共 13 条
[1]   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
[2]  
Buning Hans Kleine, 1999, Cambridge Tracts in Theoretical Computer Science, V48
[3]  
Büning HK, 2004, LECT NOTES COMPUT SC, V2919, P93
[4]  
CADOLI M, 2000, HIGHLIGHTS SATISFIAB
[5]  
FELDMANN R, 2000, P AAAI
[6]  
FLOGEL A, 1995, INFORMATION COMPUTAT, V117, P12
[7]  
Garey MR, 1979, Computers and Intractablity: A Guide to the Theoryof NP-Completeness
[8]  
GIUNCHIGLIA E, 2001, P IJCAR SIEN
[9]   THE INTRACTABILITY OF RESOLUTION [J].
HAKEN, A .
THEORETICAL COMPUTER SCIENCE, 1985, 39 (2-3) :297-308
[10]  
LETZ R, 2001, P IJCAR SIEN