SAT and #SAT solvers are essential tools in many fields of computer science, such as formal verification, artificial intelligence, and configuration analysis. However, even mature solvers can exhibit faulty behavior, such as crashes, incorrect results, or timeouts, especially when processing large and complex CNF formulas. Debugging such issues is challenging due to the size and complexity of the formulas involved. In this thesis, we present a fully automated, configurable tool that reduces fault-causing CNF formulas while preserving the faulty solver behavior. Unlike traditional simplification methods, the reduction is behavior-driven and treats solvers as black boxes, relying solely on observable outputs such as exit codes, runtime, and solver results. The tool supports three classes of solver bugs and offers a variety of features to enable configurable strategies for CNF reduction. We present an empirical evaluation using real world bugs in popular #SAT solvers (i.e., CountAntom, dSharp, and Ganak), demonstrating the tool’s effectiveness in reducing formulas significantly while maintaining the faulty solver behavior. The resulting smaller formulas enable faster debugging, clearer bug reports, and regression tests, ultimately contributing to more robust and maintainable solvers.
Manuel Dittrich (Wed,) studied this question.