Boolean Functions as Models for Quantified Boolean Formulas

被引:0
作者
Hans Kleine Büning
K. Subramani
Xishun Zhao
机构
[1] Universität Paderborn,Department of Computer Science
[2] West Virginia University,LDCSEE
[3] Sun Yat-sen University,Institute of Logic and Cognition
来源
Journal of Automated Reasoning | 2007年 / 39卷
关键词
Quantified Boolean formula; Boolean function; Model; Complexity; Satisfiability; Propositional logic;
D O I
暂无
中图分类号
学科分类号
摘要
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
页数:26
相关论文
共 11 条
  • [1] Aspvall B.(1979)A Linear-time algorithm for testing the truth of certain quantified Boolean formulas Inf. Process. Lett. 8 121-123
  • [2] Plass M.F.(1995)Resolution for quantified Boolean formulas Information and Computation. 117 12-18
  • [3] Tarjan R.E.(1985)The intractability of resolution Theor. Comp. Sci. 39 297-308
  • [4] Flögel A.(2004)On Boolean models for quantified Boolean horn formulas Italy. Lect. Notes Comput. Sci. 2919 93-104
  • [5] Karpinski M.(1977)The polynomial-time hierarchy Theor. Comp. Sci. 3 1-22
  • [6] Kleine Büning H.(undefined)undefined undefined undefined undefined-undefined
  • [7] Haken A.(undefined)undefined undefined undefined undefined-undefined
  • [8] Kleine Büning H.(undefined)undefined undefined undefined undefined-undefined
  • [9] Subramani K.(undefined)undefined undefined undefined undefined-undefined
  • [10] Zhao X.(undefined)undefined undefined undefined undefined-undefined