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
- SAT Competition 2017
(with Glucose 4.2.1)- 1nd, Parallel Track
- 2nd, Incremental Track
- 3th, Agile Track
- SAT Competition 2016
(with Glucose 4.1)- 2nd, Incremental Track
- SAT Race 2015
(with Glucose 4.0 and Glucose 4.0)- 1nd, Parallel Track
- 3th, Incremental Track
- Contest 2015
(with Glucose 3.0 and Glucose 4.0)- 2nd, Certified UNSAT, Applications
- 4th, Parallel SAT+UNSAT, Applications
- Contest 2014
(with Glucose 3.0 and Glucose 4.0- 2nd, Certified UNSAT, Applications
- 4th, Parallel SAT+UNSAT, Applications
- Contest 2013
(with Glucose 3.0)- 1st, Certified UNSAT, Applications
- 1st, SAT, Hard Combinatorial
- 2nd, Certified UNSAT, Hard Combinatorial
- 3rd, SAT+UNSAT, Hard Combinatorial
- Race 2012
(with Glucose 2.1)
- 1st, Single Engine, Application
- Contest 2011
(with Glucose 2.0)
- 1st, SAT+UNSAT, Applications
- 2nd, UNSAT, Applications
- 3rd, UNSAT, Crafted
- Contest 2009
(with Glucose 1.0)
- 1st, UNSAT, Applications
- 2nd, SAT+UNSAT, Applications
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 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.
dépot officiel https://github.com/audemard/glucose/releases/tag/4.2.1
Older versions
Glucose 4.1 2016-2017
Glucose syrup, refactoring + adaptation
- Note: Don’t change the preprocessing switches on this version (you can turn off the preprocessing but when using it, don’t play with the preprocessing options). We were reported some discrepancies in the results when using the -rcheck argument.
- This refactoring version (small simplifications in the code) fixed an issue when printing the SAT models, in the 4.0 version.
- Automated adaptation (tuned by hand) w.r.t. the kind of search the solver is doing during the first 100,000 conflicts (see our 2016 paper about that).
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 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
- Note: Don’t change the preprocessing switches on this version (you can turn off the preprocessing but when using it, don’t play with the preprocessing options). We were reported some discrepancies in the results when using the -rcheck argument.
- 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.
dépot officiel 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 thesimp
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
2012Here 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
2011Here 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
2009Here 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>
- 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 thecore
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>
How to use it? A Short guide to beginners
We are often asked how to use/install/call our SAT solver.