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

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

    Articles de conférences nationales

    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.