Glucose's Home Page

Welcome

SAT'11 Proc.

Last News

glucose v.2 released
Jul. 12, 2011

glucose v2 won 3 medals at the SAT 2011 competition
Jun. 23, 2011

SAT Conference
June 19th to 22th, 2011 (inclusive)

Don't Miss this

CP'2011
www.dmi.unipg.it/cp2011

SAT'2012
sat2012.fbk.eu/

All about the Glucose SAT Solver

Gilles and I at SAT'2011 Glucose is based on a new scoring scheme (well, not so new now) for the clause learning mechanism, based our IJCAI'09 paper. This page summarizes the techniques embedded in the competition 09 version of glucose. Solver's name is a contraction of the concept of "glue clauses", a particular kind of clauses that glucose detects and preserves during search.

Overview of glucose results in the last two competitions (2009, 2011)

Glucose was ranked 1st at the 2009 SAT competition on Applications (UNSAT) problems. It solved the same number of problems as precosat in the SAT+UNSAT category, but was ranked 2nd, due to tie-breaking on CPU time.

Glucose was ranked 1st at the 2011 SAT competition on Applications (SAT+UNSAT) problems and was in good positions in other tracks.

short analysis of glucose 2: Learning was firstly introduced for completeness. But, if we study all Glucose 2’s traces of the last competition, 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 proof as possible.

Releases

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

Here is also a very short report on the version 1.0 of glucose 1.

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

Related Paper

You should take a look at our IJCAI'09 paper for detailed results/ideas underlying this work.