A multi-engine solver for quantified Boolean formulas

被引:0
作者
Pulina, Luca [1 ]
Tacchella, Armando [1 ]
机构
[1] Univ Genoa, DIST, I-16145 Genoa, Italy
来源
PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING - CP 2007 | 2007年 / 4741卷
关键词
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
相关论文
共 24 条
[1]  
AHA DW, 1991, MACH LEARN, V6, P37, DOI 10.1007/BF00153759
[2]  
[Anonymous], 1995, 12 INT C MACH LEARN, DOI DOI 10.1016/B978-1-55860-377-6.50023-2
[3]  
ANSOTEGUI C, 2005, P AAAI
[4]  
BENEDETTI M, 2005, LNCS LNAI, P3632
[5]  
Biere A, 2005, LNCS, V3542
[6]   RESOLUTION FOR QUANTIFIED BOOLEAN-FORMULAS [J].
BUNING, HK ;
KARPINSKI, M ;
FLOGEL, A .
INFORMATION AND COMPUTATION, 1995, 117 (01) :12-18
[7]   A MACHINE PROGRAM FOR THEOREM-PROVING [J].
DAVIS, M ;
LOGEMANN, G ;
LOVELAND, D .
COMMUNICATIONS OF THE ACM, 1962, 5 (07) :394-397
[8]  
Egly U, 2000, SEVENTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-2001) / TWELFTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE (IAAI-2000), P417
[9]  
GENT IP, 2004, P 16 EUR C ART INT E
[10]  
Giunchiglia E., 2001, QUANTIFIED BOOLEAN F