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.
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Manthey, Norbert: The \textscMergeSatsolver (2021)
- Eggensperger, Katharina; Lindauer, Marius; Hutter, Frank: Pitfalls and best practices in algorithm configuration (2019)
- Eggensperger, Katharina; Lindauer, Marius; Hoos, Holger H.; Hutter, Frank; Leyton-Brown, Kevin: Efficient benchmarking of algorithm configurators via model-based surrogates (2018)
- Manthey, Norbert; Lindauer, Marius: SpyBug: automated bug detection in the configuration space of SAT solvers (2016)
- Philipp, Tobias; Rebola-Pardo, Adrián: DRAT proofs for XOR reasoning (2016)