.. _spkg_glucose:

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