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¶
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