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

共 19 条

[1]

Ansotegui Carlos, 2005, AAAI, P275

[2]

Benedetti M, 2005, LECT NOTES ARTIF INT, V3632, P369

[3]

Biere A, 2005, LECT NOTES COMPUT SC, V3542, P59

[4]

Bubeck U, 2007, LECT NOTES COMPUT SC, V4501, P244

[5] RESOLUTION FOR QUANTIFIED BOOLEAN-FORMULAS [J].

BUNING, HK ;

KARPINSKI, M ;

FLOGEL, A .

INFORMATION AND COMPUTATION, 1995, 117 (01) :12-18

[6] A COMPUTING PROCEDURE FOR QUANTIFICATION THEORY [J].

DAVIS, M ;

PUTNAM, H .

JOURNAL OF THE ACM, 1960, 7 (03) :201-215

[7]

Egly U, 2000, SEVENTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-2001) / TWELFTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE (IAAI-2000), P417

[8]

Giunchiglia E., 2001, QUANTIFIED BOOLEAN F

[9] Clause/term resolution and learning in the evaluation of Quantified Boolean Formulas [J].

Giunchiglia, Enrico ;

Narizzano, Massimo ;

Tacchella, Armando .

JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 2006, 26 :371-416

[10]

Jussila T., 2006, P 4 INT WORKSH BOUND

← 1 2 →