RESOLUTION FOR QUANTIFIED BOOLEAN-FORMULAS

被引：208
|
作者：
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 条
  • [21] FUNCTIONS COMPUTED BY MONOTONE BOOLEAN-FORMULAS WITH NO REPEATED VARIABLES
    MUNDICI, D
    [J]. THEORETICAL COMPUTER SCIENCE, 1989, 66 (01) : 113 - 114
  • [22] CRYPTOGRAPHIC LIMITATIONS ON LEARNING BOOLEAN-FORMULAS AND FINITE AUTOMATA
    KEARNS, M
    VALIANT, L
    [J]. JOURNAL OF THE ACM, 1994, 41 (01) : 67 - 95
  • [23] A Survey on Applications of Quantified Boolean Formulas
    Shukla, Ankit
    Biere, Armin
    Seidl, Martina
    Pulina, Luca
    [J]. 2019 IEEE 31ST INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE (ICTAI 2019), 2019, : 78 - 84
  • [24] Minimal false quantified Boolean formulas
    Buening, Hans Kleine
    Zhao, Xishun
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2006, PROCEEDINGS, 2006, 4121 : 339 - 352
  • [25] Backdoor Sets of Quantified Boolean Formulas
    Samer, Marko
    Szeider, Stefan
    [J]. JOURNAL OF AUTOMATED REASONING, 2009, 42 (01) : 77 - 97
  • [26] Message passing for quantified Boolean formulas
    Zhang, Pan
    Ramezanpour, Abolfazl
    Zdeborova, Lenka
    Zecchina, Riccardo
    [J]. JOURNAL OF STATISTICAL MECHANICS-THEORY AND EXPERIMENT, 2012,
  • [27] Backdoor Sets of Quantified Boolean Formulas
    Marko Samer
    Stefan Szeider
    [J]. Journal of Automated Reasoning, 2009, 42 : 77 - 97
  • [28] On Unordered BDDs and Quantified Boolean Formulas
    Janota, Mikolas
    [J]. PROGRESS IN ARTIFICIAL INTELLIGENCE, PT II, 2019, 11805 : 501 - 507
  • [29] Equivalence models for quantified Boolean formulas
    Büning, HK
    Zhao, XS
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2005, 3542 : 224 - 234
  • [30] RANDOM BOOLEAN-FORMULAS REPRESENTING ANY BOOLEAN FUNCTION WITH ASYMPTOTICALLY EQUAL PROBABILITY
    SAVICKY, P
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1988, 324 : 512 - 517
12345