Sat7 - Engineering a Modular SAT-Solver
Christian Kern, Mohammad Reza Khaleghi, Stefan Kugele, Christian Schallhart, Michael Tautschnig, Andreas Weis · 2006
As many other SAT-solvers are developed in an artful but monolithic style, we took interest in the question whether it is possible to design and implement a modular SAT-solver in a well-engineered and modular way. In particular, we are developing a framework which allows to exchange and adapt various components of the overall SAT-solver in order to match the requirements of particular problem instances. The analysis and copy-implementation of a preexisting and successful SATsolver was a natural starting point for our project. We chose minisat 1.14 [1] as guiding example, since minisat is an award-winning, yet compact solver. The reengineering of minisat resulted in an algorithmically equivalent solver which is decomposed into a number of orthogonal and exchangeable components. In the process of analyzing minisat and developing its equivalent but modular sibling, minisat7, we found a number of approaches for potential improvements. Thus, once minisat7 was running twice as long as minisat in the worst case, we started a branch from the faithful copy in order to develop our own