Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Journal articles

On the Glucose SAT solver

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.
Document type :
Journal articles
Complete list of metadata

https://hal-univ-artois.archives-ouvertes.fr/hal-03299473
Contributor : Fabien DELORME Connect in order to contact the contributor
Submitted on : Monday, February 28, 2022 - 12:54:54 PM
Last modification on : Friday, June 17, 2022 - 3:11:46 AM
Long-term archiving on: : Sunday, May 29, 2022 - 7:24:44 PM

File

preprint.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03299473, version 1

Collections

Citation

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

Share

Metrics

Record views

43

Files downloads

12