A multi-engine solver for quantified Boolean formulas

被引:0
|
作者
Pulina, Luca [1 ]
Tacchella, Armando [1 ]
机构
[1] Univ Genoa, DIST, I-16145 Genoa, Italy
关键词
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
In this paper we study the problem of yielding robust performances from current state-of-the-art solvers for quantified Boolean formulas (QBFs). Building on top of existing QBF solvers, we implement a new multi-engine solver which can inductively learn its solver selection strategy. Experimental results confirm that our solver is always more robust than each single engine, that it is stable with respect to various perturbations, and that such results can be partially explained by a handful of features playing a crucial role in our solver.
引用
收藏
页码:574 / 589
页数:16
相关论文
共 50 条
  • [1] A self-adaptive multi-engine solver for quantified Boolean formulas
    Pulina, Luca
    Tacchella, Armando
    [J]. CONSTRAINTS, 2009, 14 (01) : 80 - 116
  • [2] A self-adaptive multi-engine solver for quantified Boolean formulas
    Luca Pulina
    Armando Tacchella
    [J]. Constraints, 2009, 14 : 80 - 116
  • [3] 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
  • [4] 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
  • [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