SAT Competition 2017

Glucose Hack Track

This MiniSat Hack Track was originally introduced for the SAT 2009 competition and had a follow-up during SAT 2011 and 2013. Following this tradition but with a more up-to-date solver we organize this year the Glucose Hack Track. The 3.0 version of Glucose is used as the base solver.

The motivation of this track is twofold. On the one hand, we want to lower the threshold for Master's and PhD students to enter the SAT competition by bringing new and innovative ideas to the original Glucose solver. On the other hand, the aim is to see how far the performance of Glucose can be improved by making only minor changes to the source code. We strongly encourage usual participants to the main track (including non-students) with "hacked" Glucose solver to participate in this track.

Our motivation behind using Glucose as the base solver: Glucose is a well-known and widely adopted solver that can be seen as a canonical CDCL solver, offering an efficient (and necessary) CDCL basis and easily modifiable code. Indeed, Glucose has been often improved by introducing only minor changes to its code ("hacking it"). Furthermore, looking back at recent progresses in CDCL solvers, most of them are based on minor changes (<10 lines each): phase caching, blocked literals, and Luby series for rapid restarts.

The motivation behind competing with minor hacks is that it can help the community to detect which types of modifications pay off: in order to isolate the actual causes of improvements when modifying solvers, it is necessary to perform scientifically valid experiments on the effects of individual changes made to a solver (e.g., individual new techniques introduced to the base solver).

The size of hacks is restricted as follows: the diff between the patched and modified sources of Glucose should be less than 1000 non-space characters. You can use our edit distance tool on all modified files to count the number of modifications, which summed up should be less than 1000.