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 Constraints 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

    2014 Gilles Audemard, Laurent Simon, Lazy clause exchange policy for parallel SAT solvers in 17th International Conference on Theory and Applications of Satisfiability Testing, pp. To appear, 2014.
    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.
    2012 Gilles Audemard, Laurent Simon, Refining restarts strategies for SAT and UNSAT formulae in 18th International Conference on Principles and Practice of Constraint Programming, 2012.
    2009 Laurent Simon, Gilles Audemard, Predicting Learnt Clauses Quality in Modern SAT Solver in Twenty-first International Joint Conference on Artificial Intelligence (IJCAI'09), 2009.

    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.
    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.