AQME is an Adaptive QBF Multi-Engine, i.e., a tool that can choose among a set of QBF solvers deployed as basic engines the one which is more likely to yield optimal results with respect to the set. AQME leverages inexpensive syntactic QBF features to discriminate the best solver to run on each formula and machine learning techniques to train an internal algorithm selection engine. AQME can be freely downloaded for research and evaluation purposes (see below), and it is based on eight state-of-the-art solvers as of QBFEVAL’06, namely 2CLSQ, QUAFFLE, QUANTOR, QUBE, SKIZZO, SSOLVE and YQUAFFLE. AQME participated hors-concours in QBFEVAL’07 and, as such, it was not ranked among the regular QBFEVAL’07 competitors. However, the three versions of AQME would have ranked in the top three positions if AQME were running as a regular competitor.
AQME download (QBFEVAL ’16 version)
Please cite this paper when referencing AQME:
Luca Pulina, Armando Tacchella: A self-adaptive multi-engine solver for quantified Boolean formulas. Constraints 14(1): 80-116 (2009)