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.

License#

  • 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).

Upstream Contact#

Website: http://www.labri.fr/perso/lsimon/glucose/

Special Update/Build Instructions#

None.

Type#

optional

Dependencies#

Version Information#

package-version.txt:

4.1

Equivalent System Packages#

See https://repology.org/project/glucose/versions

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