Glucose SAT Solver

News and distribution of our SAT solver

Most recent news

(list of all news)

Three Internships + PhD Opportunities in AI !

(09 November 2022)

Thanks to the “Trustworthy AI” chair that hast just been launched in september 2022, we have three internships opportunities available, each of them with a secured PhD funding (one if...

Graduation ceremony for our Enseirb-Matmeca engineers

(28 January 2023)

On Saturday 29 January 2023, we celebrated the 2021’s graduation ceremony of Enseirb-Matmeca. It was an opportunity for each department of the school (and for the computer science department that...

Use-Case AI4Industry Awards

(20 January 2023)

AI4Industry was held from 16 to 20 January 2023 at a multitude of sites in New Aquitaine, with the support of the R3IA which I have been leading since January...

Panel discussion on a trustworthy digital world at Unesco (Université de la terre)

(26 November 2022)

As part of the “Université de la terre” 2022, organised at Unesco, Paris, I was able to take part in panelist discussion, for general audience, on the problems of trust...

The LaBRI web site was unavailale for 4 days

(21 November 2022)

Due to some important construction work around the LaBRI building, a central electrical board exploded, leading to an emergency shutdown of all (yes, all) of the Lab’s servers, including the...

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!</p>

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.

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.

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.

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.
  • </ul> </p></div> 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.

    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!

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

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

    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>