# glucose: A SAT solver¶

## Description¶

Glucose is a SAT solver.

Citing its website:

The name of the solver 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.

• nonparallel glucose: MIT

• parallel glucose-syrup: MIT modified with:

The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot be used in any competitive event (sat competitions/evaluations) without the express permission of the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event using Glucose Parallel as an embedded SAT engine (single core or not).

zlib

None.

optional

## Version Information¶

package-version.txt:

4.1


## Equivalent System Packages¶

However, these system packages will not be used for building Sage because spkg-configure.m4 has not been written for this package; see https://trac.sagemath.org/ticket/27330