Le solveur SAT Glucose

Brèves et distribution de notre solveur

Nouvelles les plus récentes

(Liste de toutes les brèves)

Glucose est (enfin) sur Github

(17 Mai 2023)

Glucose est enfin (aussi) distribué sur Github. L’idée est tout simplement de permettre les forks officiels depuis les versions de glucose. Nous le distribuions uniquement via des archives et la...

Interview dans Sud-Ouest autour de l'I.A. de confiance

(3 Mai 2023)

L’I.A. est le sujet de nombreux articles de presse depuis quelques mois. L’exposition au grand public d’outils comme chatGPT4 accèlère encore plus le besoin d’explication et de compréhension de ces...

Séjour au Simons Institute (Berkeley)

(17 Avril 2023)

Dans le cadre du programme d’invitation du Simons Institute au sujet de SAT (SAT Reunion Semester), j’ai eu le plaisir d’être invité sur un séjour long dans ce lieu mythique...

Mise en route du projet CAP-IA

(1 Avril 2023)

Le projet CAP-IA, porté par François Clautiaux (IMB) et l’Université de Bordeaux, accepté en Novembre dernier est enfin lancé. C’est un projet ambitieux dont je porte le volet en lien...

Lancement du projet Européen DIHNAMIC

(20 Mars 2023)

Le projet Dihnamic vient d’être lancé très officiellement. C’est un projet européen et régional de grande ampleur dans lequel je suis membre de “l’advisory board”. Le projet réunit 13 partenaires....

Medals of our Glucose SAT Solver in the 2017 competition

A propos de Glucose

Glucose est un solveur SAT, qui a reçu de nombreux prix, basé sur un mécanisme de notation des clauses apprises par les solveurs SAT dit “Modernes” (Vous pouvez vous référer à l’article IJCAI’09 qui introduisait ce mécanisme). La dernière version de Glucose, introduite en 2014, a été conçue pour être intrinsèquement parallèle. Depuis 2021, avec Gilles Audemard, nous travaillons à une refactorisation poussée du code.

Cette page synthétise les différentes techniques utilisées dans les versions de Glucose. Le nom du solveur est une contraction du concept de “glue clauses”, une sorte de clause particulièrement importante dans Glucose, et préservées tout au long de la recherche.

Glucose is heavily based on Minisat, so please do cite Minisat also if you want to cite Glucose. Glucose 3.0 is based on the Minisat 2.2 version. We strongly encourage you to visit the Minisat web pages, and to try the original Minisat too.

Glucose's Awards

An illustration of glucose

A (very) short analysis of Glucose performances

Learning (in CDCL algorithms) was firstly introduced for completeness. But, if we study all Glucose 2’s traces of the competition 2011, for instance, phase 2, in the categories Applications and Crafted, Glucose 2 learnt 973,468,489 clauses (sum over all traces) but removed 909,123,525 of them, i.e. more than 93% of the clauses are removed. This view is really new and contradicts previous beliefs. Thus, we thought that one of the performance keys of our solver is not only based on the identification of good clauses, but also on the removing of bad ones. As a side effect, by aggressively deleting those clauses, Glucose increases the CDCL incompleteness (keeping learnt clauses is essential for completeness). We should also emphasize here that Glucose 2 was ranked fourth on the parallel track in the SAT 2011 competition beside the fact that it was sequential. This shows that even with a single core, our solver performed better, in user time (not CPU) than many parallel solvers exploiting the 8 cores of the parallel machine. One of the reasons for this is that Glucose 2 is good at finding the shortest (but easiest) proof as possible.

Among the short list of programs of Prof. Don Knuth, you may want to take a deep look at the SAT13.w, his CDCL implementation. Very interesting and insightful. With glucose-techniques inside!

Glucose is developed by a very friendly team: Gilles Audemard and myself. Above is the picture we took during the SAT’2011 conference at Ann Arbor (while visiting the Ford manufactory).

Last Release Download the last version

Glucose 4.2.1

This is the last official release of Glucose. We used the same unmodified version for a few competitions now. This is the release of glucose that was first used for the SAT Competition 2018 and then also for SAT-Race 2019.

Here is the source code of Glucose 4.2.1 (glucose-syrup). The main modifications are based on the extension of the LCM strategies proposed at IJCAI 2017, which ”revived” the vivification technique). You may want to read the companion short paper published in the SAT 2018 booklet to better understand this version.

dépot officiel https://github.com/audemard/glucose/releases/tag/4.2.1

Older versions

Glucose 4.1

Glucose syrup, refactoring + adaptation

Here is the source of Glucose 4.1 (glucose-syrup), the refactorized, parallel version that participated to the 2015-2017 contests. You can also download the source submitted to the contest but we worked to clean the code, so please do prefer this version. You may want to read the companion short paper published in the SAT 2016 booklet to better understand this version.

dépot officiel https://github.com/audemard/glucose/releases/tag/4.1

Glucose 4.0

Glucose is now parallel!

Here is the source code of Glucose 4.0 (glucose-syrup), the cleaned, refactorized, parallel version that participated to the 2014 contest in the parallel track. Of course, you can download the exact version submitted to the contest directly on the contest web site, but we strongly encourage you to use this version instead.

dépot officiel https://github.com/audemard/glucose/releases/tag/4.0

Older Releases Download your version

Glucose 3.0 (Last Sequential only Version)

What's new in this version?

  • We don't use anymore the Satelite external preprocessor. We rely on the simp directory, preprocessing the instance right in Glucose (thanks to the mechanism already implemented in Minisat).
  • We have included two new operating mode:
    • Certified UNSAT, you can output the proof for UNSAT and independently check it (thanks to Marijn Heule implementation of the DRUP trace).
    • Incremental mode of operation, when you want to use Glucose inside a MUS extractor, for instance, or any other Incremental SAT Solving solver. We experimented a significant gain by using our new version of incremental Glucose w.r.t. the previous one (see our paper below about Incremental SAT Solving).
    • A few other optimisations, as described in the SAT competition 2013 Companion Paper.
    • Too bad we don't have any In-Processing techniques. 2013 was the year of this new technique in SAT solvers.
    • Note: The default mode of Glucose now doesn't print the final Model if SAT. You have to use -model to turn it on now.

    Here is the source code of Glucose 3.0, the version that participated to the 2013 contest, but with cleaned code. You can download the exact version submitted to the contest directly on the contest web site, but we strongly encourage you to use this version instead.

    dépot officiel https://github.com/audemard/glucose/releases/tag/3.0

    Glucose 2.1

    Here is the source code of Glucose 2.1, the cleaned version of the one that participated to the SAT 2012 Challenge. Comments and feedbacks welcome!

    dépot officiel https://github.com/audemard/glucose/releases/tag/2.1

    Glucose 2.0

    Here is the source code of Glucose 2.0, as it was submitted to the 2011 contest (sorry, again, for the lack of comments).

    dépot officiel https://github.com/audemard/glucose/releases/tag/2.0

    Glucose 1.0

    Here is the source code of Glucose 1.0as it was submitted to the 2009 contest (sorry, again, for the lack of comments).

    dépot officiel https://github.com/audemard/glucose/releases/tag/1.0

    Related Paper More informations!

    You should take a look at our IJCAI'09 paper for detailed results/ideas underlying this work.
    • Predicting Learnt Clauses Quality in Modern SAT Solver. G. Audemard, L. Simon, in Twenty-first International Joint Conference on Artificial Intelligence (IJCAI'09), july 2009.
    • Refining restarts strategies for SAT and UNSAT formulae. Gilles Audemard and Laurent Simon, in Proceedings of the 22nd International Conference on Principles and Practice of Constraint Programming (CP-12), 2012.
    • GLUCOSE 2.1: Aggressive – but Reactive – Clause Database Management, Dynamic Restarts. In Pragmatics of SAT (Workshop of SAT'12), Gilles Audemard and Laurent Simon, Juin 2012.
    • Improving Glucose for Incremental SAT Solving with Assumption: Application to MUS Extraction. Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, in Proceedings of SAT 2013, 2013.
    • Lazy Clause Exchange Policy for parallel SAT solvers. Gilles Audemard, Laurent Simon, in 17th International Conference on Theory and Applications of Satisfiability Testing (SAT'14), 2014.
    • </ul>

      How to use it? A Short guide to beginners

      We are often asked how to use/install/call our SAT solver.

      • Don't forget to install the libz library. It is needed to read .cnf.gz files (compressed cnf). This is probably the most frequent compilation error.
      • You should type "make" into the simp (if you want to preprocess the file) or into the core directory.
      • You may have a few warning (depending on your gcc version) but this should not hurt
      • If Glucose compiles, you need now a CNF file to give it. CNF files are in Dimacs format, i.e. variables are numbers only and the formula is in conjunctive normal form. You may need to spend some time to search the web for this format. It is simple but you may need to write a few lines to handle it/play with it inside your own tool
      • If everything's ok, and if Glucose found an answer to your problem, send us an email (we like to hear successes stories about glucose ) and now you have either
        • To trust Glucose if it says "UNSAT" (your formula has no solution)
        • To run Glucose again with certified UNSAT activated (to check that glucose was correctly answer UNSAT)
        • To read the solution, if Glucose says "SAT". Your solution (with -model activated is printed at the end). </ul>
        • You may also want to take a look at the Minisat help pages </ul> </p>