On the Glucose SAT solver - Archive ouverte HAL Access content directly
Journal Articles International Journal on Artificial Intelligence Tools (IJAIT) Year : 2018

On the Glucose SAT solver

(1) , (2)
1
2

Abstract

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.
Fichier principal
Vignette du fichier
preprint.pdf (463.89 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03299473 , version 1 (28-02-2022)

Identifiers

  • HAL Id : hal-03299473 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More