Glucose est un prouveur SAT basé sur Minisat développé par Gilles Audemard et Laurent Simon intégrant sur la notion de LBD (Literal Block Distance).

Glucose est un prouveur de l’état de l’art dans la résolution pratique de SAT : il a obtenu pas moins de 9 médailles (4 or, 3 argent et 2 bronze) lors des trois dernières compétitions internationales de prouveurs SAT.

Télécharger la version 4.1


Auteurs :
Laurent Simon
Gilles Audemard

MIT    Toute catégorie    Logiciels pérennes    Prouveurs CSP & SAT   

    • Aller sur la page web du logiciel

    Code source

    Articles de revues internationales

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

    Articles de conférences internationales

    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.

    Articles de conférences nationales

    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, Du Glucose en goutte à goutte pour les coeurs inconsistants in Journées Francophones de Programmation par Contraintes, 2013.