Award-winning glucose Home Page

A SAT solver that predicts learnt-clause usefulness

Last update: July 14 2009 23:26:21.

G. Audemard and L. Simon

glucose is based on a new scoring scheme 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 comes from glue clauses, a particular kind of clauses that glucose detects and preserves during search.

glucose was ranked 1st at the 2009 SAT competition on Industrial (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.

Source code

Here is the source code submitted to the 2009 contest. A cleaned version will be released in a very few days.

Papers

you should take a look at our IJCAI'09 paper (available at the end of the conference) for detailed results/ideas.

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