Glucose is based on a new scoring scheme (well, not so new now, it was introduced in 2009) for the clause learning mechanism of so called “Modern” SAT sovlers (it is based our IJCAI'09 paper). It is designed to be parallel, since 2014. This page summarizes the techniques embedded in all the versions of glucose. The name of the Solver name is a contraction of the concept of “glue clauses”, a particular kind of clauses that glucose detects and preserves during search.

Download v 4.1


Authors :
Laurent Simon
Gilles Audemard

MIT    Any category    Perennial software   

    • Go to the software webpage

    Source code

    International journals

    2018 Gilles Audemard, Laurent Simon, On the Glucose SAT solver in International Journal on Artificial Intelligence Tools (IJAIT), vol. 27, n° 1, pp. 1-25, 2018.

    International conferences

    2013 Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, Du glucose en goutte à goutte pour les coeurs insatisfiables in 9ièmes Journées Francophones de Programmation par Contraintes (JFPC'13), pp. 59-66, 2013.
    2013 Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction in International Conference on Theory and Applications of Satisfiability Testing, 2013.
    2012 Gilles Audemard, Laurent Simon, GLUCOSE 2.1: Aggressive, but Reactive, Clause Database Management, Dynamic Restarts (System Description) in Pragmatics of SAT 2012 (POS'12), 2012.

    National conferences

    2013 Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, Du Glucose en goutte à goutte pour les coeurs inconsistants in Journées Francophones de Programmation par Contraintes, 2013.