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.
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.
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. Here is the picture we took during the SAT'2011 conference at Ann Arbor (while visiting the Ford manufactory).
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.
Glucose syrup, refactoring + adaptation
Here is the source code of Glucose 4.1 (glucose-syrup) , the refactorized, parallel version that participated to the 2015-2016 contests. You can also download the source submitted to the contest but we worked to clean the code, so please do prefer this version.
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.
What's new in this version?
Satelite
external preprocessor. We
rely on the simp
directory, preprocessing the instance right in
Glucose (thanks to the mechanism already implemented in Minisat).-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.
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!
Here is the source code of Glucose 2.0 , as it was submitted to the 2011 contest (sorry, again, for the lack of comments).
Here is the source code of Glucose 1.0 , as it was submitted to the 2009 contest (sorry, again, for the lack of comments).
You should take a look at our IJCAI'09 paper for detailed results/ideas underlying this work.
We are often asked how to use/install/call our SAT solver.
libz
library. It is needed to read .cnf.gz
files (compressed cnf). This is probably the most frequent compilation error.simp
(if you want to preprocess the file) or into the core
directory.
-model
activated is printed at the end).