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 条
  • [21] Equivalence models for quantified Boolean formulas
    Büning, HK
    Zhao, XS
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2005, 3542 : 224 - 234
  • [22] On Unordered BDDs and Quantified Boolean Formulas
    Janota, Mikolas
    [J]. PROGRESS IN ARTIFICIAL INTELLIGENCE, PT II, 2019, 11805 : 501 - 507
  • [23] Looking algebraically at tractable quantified Boolean formulas
    Chen, HB
    Dalmau, V
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2005, 3542 : 71 - 79
  • [24] Computing Smallest MUSes of Quantified Boolean Formulas
    Niskanen, Andreas
    Mustonen, Jere
    Berg, Jeremias
    Jarvisalo, Matti
    [J]. LOGIC PROGRAMMING AND NONMONOTONIC REASONING, LPNMR 2022, 2022, 13416 : 301 - 314
  • [25] A Dichotomy Theorem for Learning Quantified Boolean Formulas
    Víictor Dalmau
    [J]. Machine Learning, 1999, 35 : 207 - 224
  • [26] Abstract Solvers for Quantified Boolean Formulas and their Applications
    Brochenin, Remi
    Maratea, Marco
    [J]. AI*IA 2015: ADVANCES IN ARTIFICIAL INTELLIGENCE, 2015, 9336 : 205 - 217
  • [27] A Structural Approach to Reasoning with Quantified Boolean Formulas
    Pulina, Luca
    Tacchella, Armando
    [J]. 21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS, 2009, : 596 - 602
  • [28] Extracting Certificates from Quantified Boolean Formulas
    Benedetti, Marco
    [J]. 19TH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-05), 2005, : 47 - 53
  • [29] QuBIS: An (In)complete Solver for Quantified Boolean Formulas
    Pulina, Luca
    Tacchella, Armando
    [J]. MICAI 2008: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2008, 5317 : 34 - 43
  • [30] Moving Definition Variables in Quantified Boolean Formulas
    Reeves, Joseph E.
    Heule, Marijn J. H.
    Bryant, Randal E.
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT I, 2022, 13243 : 462 - 479
12345