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 条
  • [31] Quantifier Shifting for Quantified Boolean Formulas Revisited
    Heisinger, Simone
    Heisinger, Maximilian
    Rebola-Pardo, Adrian
    Seidl, Martina
    [J]. AUTOMATED REASONING, IJCAR 2024, PT I, 2024, 14739 : 325 - 343
  • [32] A dichotomy theorem for learning quantified boolean formulas
    Dalmau, V
    [J]. MACHINE LEARNING, 1999, 35 (03) : 207 - 224
  • [33] A Model for Generating Random Quantified Boolean Formulas
    Chen, Hubie
    Interian, Yannet
    [J]. 19TH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-05), 2005, : 66 - 71
  • [34] Propositional PSPACE reasoning with boolean programs versus quantified Boolean formulas
    Skelley, A
    [J]. AUTOMATA , LANGUAGES AND PROGRAMMING, PROCEEDINGS, 2004, 3142 : 1163 - 1175
  • [35] A symbolic search based approach for quantified Boolean formulas
    Audemard, G
    Saïs, L
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, PROCEEDINGS, 2005, 3569 : 16 - 30
  • [36] Expressing default abduction problems as quantified Boolean formulas
    Tompits, H
    [J]. AI COMMUNICATIONS, 2003, 16 (02) : 89 - 105
  • [37] A multi-engine solver for quantified Boolean formulas
    Pulina, Luca
    Tacchella, Armando
    [J]. PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING - CP 2007, 2007, 4741 : 574 - 589
  • [38] Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas
    Egly, Uwe
    Woltran, Stefan
    [J]. COMPUTATIONAL MODELS OF ARGUMENT, 2006, 144 : 133 - 144
  • [39] FORMULAS, REGULAR LANGUAGES AND BOOLEAN CIRCUITS
    PELADEAU, P
    [J]. THEORETICAL COMPUTER SCIENCE, 1992, 101 (01) : 133 - 141
  • [40] Transforming Quantified Boolean Formulas Using Biclique Covers
    Kullmann, Oliver
    Shukla, Ankit
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2023, 2023, 13994 : 372 - 390
12345