SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers

authored by

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.

External Organisation(s)

University of Freiburg

Type

Conference contribution

Pages

215-222

No. of pages

8

Publication date

27.10.2015

Publication status

Published

Peer reviewed

Yes

ASJC Scopus subject areas

Theoretical Computer Science, Computer Science(all)

Electronic version(s)

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