Glucose SAT Solver

News and distribution of our SAT solver

Most recent news

(list of all news)

Glucose is (finally) on Github

(17 May 2023)

Glucose is finally (also) distributed on Github. The idea is simply to allow official forks from Glucose versions. We used to distribute it only via the archives and the official...


Interview in the Regional Newspaper "Sud-Ouest" about Trustworthy AI

(03 May 2023)

A.I. has been the subject of many, many press articles in recent months. The exposure of tools such as chatGPT4 to the general public accelerates even more the need for...


Invitation to the Simons Institute (Berkeley)

(17 April 2023)

As part of the Simons Institute’s SAT Program (SAT Reunion Semester), I had the pleasure of being invited for a long stay in this famous research place about theoretical computer...


Lauch of the DIHNAMIC European Project

(20 March 2023)

The Dihnamic project has just been launched very officially. It is a large-scale European and regional project in which I act as a member of the advisory board. The project...


Dataquitaine 2023

(02 March 2023)

The sixth “Dataquitaine” (a regional scientific event organized in Nouvelle-Aquitaine) days were held on Thursday 2 March 2023 at Kedge Business School, organised by Digital Aquitaine and especially the Domex...

Medals of our Glucose SAT Solver in the 2017 competition

About Glucose

Glucose is an award winning SAT solver based on a scoring scheme we introduced in 2009 for the clause learning mechanism of so called “Modern” SAT sovlers (see our IJCAI’09 paper). It is designed to be parallel, since 2014 and was enterly rebooted in 2021. Glucose is coded and maintened since its beginning by Gilles Audemard and myself.

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.

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


We officially set up a Github repository for Glucoe

We are keeping all the previous versions of glucose (Zip, Tar) below but from now on, the official link for the Glucose SAT solver is its Github repository https://github.com/audemard/glucose

You can access to all versions of Glucose thanks to tags!

Last Release Download the last version

Glucose 4.2.1
2018

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.

repository https://github.com/audemard/glucose/releases/tag/4.2.1

Older versions

Glucose 4.1
2016-2017

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.

repository https://github.com/audemard/glucose/releases/tag/4.1

Glucose 4.0
2014

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.

repository https://github.com/audemard/glucose/releases/tag/4.0


Older Releases Download your version

Glucose 3.0 (Last Sequential only Version)
2013

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.
    repository https://github.com/audemard/glucose/releases/tag/3.0

    Glucose 2.1
    2012

    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!


    repository https://github.com/audemard/glucose/releases/tag/2.1

    Glucose 2.0
    2011

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


    repository https://github.com/audemard/glucose/releases/tag/2.0

    Glucose 1.0
    2009

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

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