RESOLUTION FOR QUANTIFIED BOOLEAN-FORMULAS

被引：209
|
作者：
BUNING, HK [1 ]
KARPINSKI, M [1 ]
FLOGEL, A [1 ]
机构：
[1] UNIV BONN, INST INFORMAT, D-53012 BONN, GERMANY
来源：
INFORMATION AND COMPUTATION | 1995年 / 117卷 / 01期
关键词：
D O I：
10.1006/inco.1995.1025
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
A complete and sound resolution operation directly applicable to the quantified Boolean formulas is presented. If we restrict the resolution to unit resolution, then the completeness and soundness for extended quantified Horn formulas is shown. We prove that the truth of a quantified Horn formula can be decided in O(rn) time, where n is the length of the formula and r is the number of universal variables, whereas in contrast the evaluation problem for extended quantified Horn formulas is coNP-complete for formulas with prefix For All There Exists. Further, we show that the resolution is exponential for extended quantified Horn formulas. (C) 1995 Academic Press, Inc.
引用
收藏
页码：12 / 18
页数：7
相关论文
共 50 条
  • [1] SUBCLASSES OF QUANTIFIED BOOLEAN-FORMULAS
    FLOGEL, A
    KARPINSKI, M
    BUNING, HK
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 533 : 145 - 155
  • [2] LEARNING BOOLEAN-FORMULAS
    KEARNS, M
    LI, M
    VALIANT, L
    JOURNAL OF THE ASSOCIATION FOR COMPUTING MACHINERY, 1994, 41 (06): : 1298 - 1328
  • [3] BOOLEAN-FORMULAS AND FAMILIES OF SETS
    MIESCICKI, J
    BULLETIN OF THE POLISH ACADEMY OF SCIENCES-CHEMISTRY, 1994, 42 (01): : 111 - 123
  • [4] Variable independence and resolution paths for quantified boolean formulas
    Van Gelder, Allen
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2011, 6876 LNCS : 789 - 803
  • [5] Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits
    Buening, Hans Kleine
    Zhao, Xishun
    Bubeck, Uwe
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2009, PROCEEDINGS, 2009, 5584 : 391 - +
  • [6] OPTIMAL VERSUS STABLE IN BOOLEAN-FORMULAS
    JUKNA, S
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 529 : 265 - 274
  • [7] IMPROVED BOOLEAN-FORMULAS FOR THE RAMSEY GRAPHS
    SAVICKY, P
    RANDOM STRUCTURES & ALGORITHMS, 1995, 6 (04) : 407 - 415
  • [8] Clause/term resolution and learning in the evaluation of quantified boolean formulas
    Giunchiglia, Enrico
    Narizzano, Massimo
    Tacchella, Armando
    Journal of Artificial Intelligence Research, 2006, 26 : 371 - 416
  • [9] Clause/term resolution and learning in the evaluation of Quantified Boolean Formulas
    Giunchiglia, Enrico
    Narizzano, Massimo
    Tacchella, Armando
    JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 2006, 26 : 371 - 416
  • [10] SIZE-DEPTH TRADEOFFS FOR BOOLEAN-FORMULAS
    BONET, ML
    BUSS, SR
    INFORMATION PROCESSING LETTERS, 1994, 49 (03) : 151 - 155
12345