SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers

Automated configuration is used to improve the performance of a SAT solver. Increasing the space of possible parameter configurations leverages the power of configuration but also leads to harder maintainable code and to more undiscovered bugs. We present the tool SpyBug that finds erroneous minimal parameter configurations of SAT solvers and their parameter specification to help developers to identify and narrow down bugs in their solvers. The importance of SpyBug is shown by the bugs we found for four well-known SAT solvers that won prices in international competitions.