A self-adaptive multi-engine solver for quantified Boolean formulas |
| |
Authors: | Luca Pulina Armando Tacchella |
| |
Affiliation: | (1) DIST, Università di Genova, Viale Causa, 13-16145 Genova, Italy |
| |
Abstract: | In this paper we study the problem of engineering a robust solver for quantified Boolean formulas (QBFs), i.e., a tool that
can efficiently solve formulas across different problem domains without the need for domain-specific tuning. The paper presents
two main empirical results along this line of research. Our first result is the development of a multi-engine solver, i.e.,
a tool that selects among its reasoning engines the one which is more likely to yield optimal results. In particular, we show
that syntactic QBF features can be correlated to the performances of existing QBF engines across a variety of domains. We
also show how a multi-engine solver can be obtained by carefully picking state-of-the-art QBF solvers as basic engines, and
by harnessing inductive reasoning techniques to learn engine-selection policies. Our second result is the improvement of our
multi-engine solver with the capability of updating the learned policies when they fail to give good predictions. In this
way the solver becomes also self-adaptive, i.e., able to adjust its internal models when the usage scenario changes substantially.
The rewarding results obtained in our experiments show that our solver AQME—Adaptive QBF Multi-Engine—can be more robust and
efficient than state-of-the-art single-engine solvers, even when it is confronted with previously uncharted formulas and competitors. |
| |
Keywords: | Self-adaptive multi-engine solver Quantified Boolean formulas AQME |
本文献已被 SpringerLink 等数据库收录! |
|