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/

Dependencies

zlib

Special Update/Build Instructions

None.

Type

optional

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 https://trac.sagemath.org/ticket/27330