Improving Implementation of SAT Competitions 2017–2019 Winners

The results of annual SAT competitions are often viewed as the milestones showcasing the progress in SAT solvers. However, their competitive nature leads to the situation when the majority of this year’s solvers are based on previous year’s winner. And since the main focus is always on novelty, it means that there are times when some implementation details have a potential for improvement, but they are just inherited from solver to solver for several years in a row. In this study we propose small modifications of implementations of existing heuristics in several related SAT solvers. These modifications mostly consist in employing a deterministic strategy for switching between branching heuristics and in augmentations of the treatment of Tier2 and Core clauses. In our experiments we show that the proposed changes have a positive effect on solvers’ performance both individually and in combination with each other.