Tags:continuous integration, incremental sat solving, SAT solver, satisfiability testing and solver development
Abstract:
Successful SAT solvers in recent competitions are typically based on the winner of the previous competition. Due to this procedure, for multiple years relevant features like incremental solving have not been supported by winning solvers anymore. Furthermore, bug fixes in one solver do not evolve into predecessors. This work presents MergeSat, a SAT solver that is also based on leading solvers of the past years. However, MergeSat can replace MiniSat or Glucose, as relevant features have been added back. Also, new techniques from other solvers of the community have been adapted, and implementation issues have been identified and fixed. These issues did not surface in an original solver or its successor during competitions. Finally, we provide a mechanism to easily incorporate changes of other solver, as well as a development and test environment to identify potential issues when merging techniques early. With this setup, MergeSat is a good starting point for future research development and integration into other solvers.