The Glucose SAT Solver

Glucose is based on a new scoring scheme (well, not so new now, it was introduced in 2009) for the clause learning mechanism of so called "Modern" SAT sovlers (it is based our IJCAI'09 paper). It is designed to be parallel, since 2014. 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.

Awards


Minisat

Glucose was made possible with the tremendous work done by Niklas & Niklas with Minisat. 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.


D. Knuth and Glucose

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!


Goodie

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

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


Last Release Download the last version

Glucose 4.0 (Last Version) New
2014

Glucose is now parallel!

  • You can call it Glucose Parallel or Glucose-Syrup (a lot of glucose in it).
  • Major refactoring of Glucose: Only one source for parallel and sequential solver.
  • An original mechanism for clause sharing (as described in the SAT 2014 paper, based on a 1-Watched literal scheme).
  • Can work with a lot of cores and limited memory
  • Very good performances on industrial (non crypto) problems
  • No determinism in the parallel version
  • You can choose to compile the following Glucose derivates:
    • Glucose sequential (with/without Satelite, decided by command line arguments)
    • Glucose sequential, incremental mode
    • Glucose sequential, certified unsat proof logging
    • Glucose parallel with satelite ( not yet a parallel certified unsat / parallel incremental)
  • Choose your directory (simp or parallel) and type 'make'

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


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!


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


Glucose 1.0
2009

Here is the source code of Glucose 1.0 , as 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.


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).
  • You may also want to take a look at the Minisat help pages