Advertisement
Published in:
2015 | OriginalPaper | Chapter
SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
Authors : Stefan Falkner, Marius Lindauer, Frank Hutter
Published in: Theory and Applications of Satisfiability Testing -- SAT 2015
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.