QuBIS: An (In)complete Solver for Quantified Boolean Formulas

被引：0
|
作者：
Pulina, Luca [1 ]
Tacchella, Armando [1 ]
机构：
[1] Univ Genoa, DIST, I-16145 Genoa, Italy
来源：
MICAI 2008: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS | 2008年 / 5317卷
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
In this paper we introduce QUBIS an (in)complete solver for quantified Boolean formulas (QBFs). The particularity of QUBIS is that it is not inherently incomplete, but it has the ability to surrender upon realizing that; its deduction mechanism is becoming ineffective. Whenever this happens, QUBIS outputs a partial result which can be fed to a complete QBF solver for further processing. As our experiments show; not only QUBIS is competitive as an incomplete solver, but providing the output of QUBIS as an input to complete solvers can boost their performances on several instances.
引用
收藏
页码：34 / 43
页数：10
相关论文
共 50 条
  • [1] 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
  • [2] SAT based BDD solver for Quantified Boolean Formulas
    Audemard, G
    Saïs, L
    [J]. ICTAI 2004: 16TH IEEE INTERNATIONALCONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2004, : 82 - 89
  • [3] A self-adaptive multi-engine solver for quantified Boolean formulas
    Pulina, Luca
    Tacchella, Armando
    [J]. CONSTRAINTS, 2009, 14 (01) : 80 - 116
  • [4] A self-adaptive multi-engine solver for quantified Boolean formulas
    Luca Pulina
    Armando Tacchella
    [J]. Constraints, 2009, 14 : 80 - 116
  • [5] Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver
    Bryant, Randal E.
    Heule, Marijn J. H.
    [J]. AUTOMATED DEDUCTION, CADE 28, 2021, 12699 : 433 - 449
  • [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] 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
  • [10] On Boolean models for Quantified Boolean Horn formulas
    Büning, HK
    Subramani, K
    Zhao, XS
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2004, 2919 : 93 - 104
12345