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 条
  • [41] SAT based BDD solver for Quantified Boolean Formulas
    Audemard, G
    Saïs, L
    ICTAI 2004: 16TH IEEE INTERNATIONALCONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2004, : 82 - 89
  • [42] FORMULAS, REGULAR LANGUAGES AND BOOLEAN CIRCUITS
    PELADEAU, P
    THEORETICAL COMPUTER SCIENCE, 1992, 101 (01) : 133 - 141
  • [43] Partial Witnesses from Preprocessed Quantified Boolean Formulas
    Seidl, Martina
    Koenighofer, Robert
    2014 DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION (DATE), 2014,
  • [44] Comparing different prenexing strategies for quantified Boolean formulas
    Egly, U
    Seidl, M
    Tompits, H
    Woltran, S
    Zolda, M
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2004, 2919 : 214 - 228
  • [45] A Duality-Aware Calculus for Quantified Boolean Formulas
    Fazekas, Katalin
    Seidl, Martina
    Biere, Armin
    PROCEEDINGS OF 2016 18TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC), 2016, : 181 - 186
  • [46] Short proofs for some symmetric Quantified Boolean Formulas
    Kauers, Manuel
    Seidl, Martina
    INFORMATION PROCESSING LETTERS, 2018, 140 : 4 - 7
  • [47] On computing belief change operations using quantified Boolean formulas
    Delgrande, JP
    Schaub, T
    Tompits, H
    Woltran, S
    JOURNAL OF LOGIC AND COMPUTATION, 2004, 14 (06) : 801 - 826
  • [48] Primal and Dual Encoding from Applications into Quantified Boolean Formulas
    Van Gelder, Allen
    PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING, CP 2013, 2013, 8124 : 694 - 707
  • [49] Solving dependency quantified Boolean formulas using quantifier localization
    Ge-Ernst, Aile
    Scholl, Christoph
    Sic, Juraj
    Wimmer, Ralf
    THEORETICAL COMPUTER SCIENCE, 2022, 925 : 1 - 24
  • [50] Solving advanced reasoning tasks using quantified Boolean formulas
    Egly, U
    Eiter, T
    Tompits, H
    Woltran, S
    SEVENTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-2001) / TWELFTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE (IAAI-2000), 2000, : 417 - 422
12345