On the Glucose SAT solver

Gilles Audemard (1) , Laurent Simon (2)

1 CRIL - Centre de Recherche en Informatique de Lens
2 LaBRI - Laboratoire Bordelais de Recherche en Informatique

The set of novelties introduced with the SAT solver Glucose is now considered as a standard for practical SAT solving. In this paper, we review the different strategies and technologies added in Glucose over the years. We detail each technique and discuss its impact on the final performances reached by Glucose. We also come back on one of the main developments of the solver over the very last years: its efficient parallelization. We extensively tested different versions of Glucose and Syrup (its parallel version) on a l the benchmarks since 2011. By including, as a reference, the SAT solver Lingeling (and its parallel version Plingeling), we show that Glucose and Syrup are significantly faster than other solvers, even if they can solve fewer instances.

Domaines: Intelligence artificielle [cs.AI]

Gilles Audemard, Laurent Simon. On the Glucose SAT solver. International Journal on Artificial Intelligence Tools (IJAIT), 2018, 27 (1), pp.1-25. ⟨hal-03299473⟩