user

Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits

被引：0
|
作者：
Buening, Hans Kleine [1 ]
Zhao, Xishun [2 ]
Bubeck, Uwe [1 ]
机构：
[1] Univ Paderborn, Paderborn, Germany
[2] Sun Yat Sen Univ, Guangzhou, Peoples R China
来源：
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2009, PROCEEDINGS | 2009年 / 5584卷
关键词：
HORN;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present an extension of Q-Unit resolution for formulas that are not completely in clausal form. This b-unit resolution is applied to different classes of quantified Boolean formulas in which the existential and universal variables satisfy the Horn property. These formulas are transformed into propositional equivalents consisting of only polynomially many subformulas. We obtain compact encodings as Boolean circuits and show that both representations have the same expressive power.
引用
收藏
页码：391 / +
页数：3
相关论文
共 50 条
  • [1] SUBCLASSES OF QUANTIFIED BOOLEAN-FORMULAS
    FLOGEL, A
    KARPINSKI, M
    BUNING, HK
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 533 : 145 - 155
  • [2] RESOLUTION FOR QUANTIFIED BOOLEAN-FORMULAS
    BUNING, HK
    KARPINSKI, M
    FLOGEL, A
    [J]. INFORMATION AND COMPUTATION, 1995, 117 (01) : 12 - 18
  • [3] Variable independence and resolution paths for quantified boolean formulas
    Van Gelder, Allen
    [J]. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2011, 6876 LNCS : 789 - 803
  • [4] Clause/term resolution and learning in the evaluation of quantified boolean formulas
    Giunchiglia, Enrico
    Narizzano, Massimo
    Tacchella, Armando
    [J]. Journal of Artificial Intelligence Research, 2006, 26 : 371 - 416
  • [5] Clause/term resolution and learning in the evaluation of Quantified Boolean Formulas
    Giunchiglia, Enrico
    Narizzano, Massimo
    Tacchella, Armando
    [J]. JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 2006, 26 : 371 - 416
  • [6] On models for quantified Boolean formulas
    Büning, HK
    Zhao, XS
    [J]. LOGIC VERSUS APPROXIMATION: ESSAYS DEDICATED TO MICHAEL M RICHTER ON THE OCCASION OF HIS 65TH BIRTHDAY, 2004, 3075 : 18 - 32
  • [7] Symmetries of Quantified Boolean Formulas
    Kauers, Manuel
    Seidl, Martina
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2018, 2018, 10929 : 199 - 216
  • [8] Algorithms for quantified Boolean formulas
    Williams, R
    [J]. PROCEEDINGS OF THE THIRTEENTH ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS, 2002, : 299 - 307
  • [9] Reasoning with quantified boolean formulas
    Giunchiglia, Enrico
    Marin, Paolo
    Narizzano, Massimo
    [J]. Frontiers in Artificial Intelligence and Applications, 2009, 185 (01) : 761 - 780
  • [10] Boolean functions as models for quantified Boolean formulas
    Buening, Hans Kleine
    Subramani, K.
    Zhao, Xishun
    [J]. JOURNAL OF AUTOMATED REASONING, 2007, 39 (01) : 49 - 75
12345