SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers

verfasst von

Stefan Falkner, Marius Lindauer, Frank Hutter

Abstract

Most modern SAT solvers expose a range of parameters to allow some customization for improving performance on specific types of instances. Performing this customization manually can be challenging and time-consuming, and as a consequence several automated algorithm configuration methods have been developed for this purpose. Although automatic algorithm configuration has already been applied successfully to many different SAT solvers, a comprehensive analysis of the configuration process is usually not readily available to users. Here, we present SpySMAC to address this gap by providing a lightweight and easy-to-use toolbox for (i) automatic configuration of SAT solvers in different settings, (ii) a thorough performance analysis comparing the best found configuration to the default one, and (iii) an assessment of each parameter’s importance using the fANOVA framework. To showcase our tool, we apply it to Lingeling and probSAT, two state-of-the-art solvers with very different characteristics.

Externe Organisation(en)

Albert-Ludwigs-Universität Freiburg

Typ

Aufsatz in Konferenzband

Seiten

215-222

Anzahl der Seiten

8

Publikationsdatum

27.10.2015

Publikationsstatus

Veröffentlicht

Peer-reviewed

Ja

ASJC Scopus Sachgebiete

Theoretische Informatik, Informatik (insg.)

Elektronische Version(en)

https://doi.org/10.1007/978-3-319-24318-4_16 (Zugang: Geschlossen)