Feature for testing the presence of SAT solvers

class sage.features.sat.Glucose(*args, **kwds)[source]

Bases: Executable

A Feature describing the presence of an executable from the Glucose SAT solver.

EXAMPLES:

sage: from sage.features.sat import Glucose
sage: Glucose().is_present()                  # optional - glucose
FeatureTestResult('glucose', True)
>>> from sage.all import *
>>> from sage.features.sat import Glucose
>>> Glucose().is_present()                  # optional - glucose
FeatureTestResult('glucose', True)
class sage.features.sat.Kissat(*args, **kwds)[source]

Bases: Executable

A Feature describing the presence of the Kissat SAT solver.

EXAMPLES:

sage: from sage.features.sat import Kissat
sage: Kissat().is_present()                             # optional - kissat
FeatureTestResult('kissat', True)
>>> from sage.all import *
>>> from sage.features.sat import Kissat
>>> Kissat().is_present()                             # optional - kissat
FeatureTestResult('kissat', True)
class sage.features.sat.Pycosat(*args, **kwds)[source]

Bases: PythonModule

A Feature describing the presence of pycosat: SAT solver picosat with Python bindings.

EXAMPLES:

sage: from sage.features.sat import Pycosat
sage: Pycosat().is_present()                  # optional - pycosat
FeatureTestResult('pycosat', True)
>>> from sage.all import *
>>> from sage.features.sat import Pycosat
>>> Pycosat().is_present()                  # optional - pycosat
FeatureTestResult('pycosat', True)
class sage.features.sat.Pycryptosat(*args, **kwds)[source]

Bases: PythonModule

A Feature describing the presence of pycryptosat: Python module of cryptominisat.

EXAMPLES:

sage: from sage.features.sat import Pycryptosat
sage: Pycryptosat().is_present()              # optional - pycryptosat
FeatureTestResult('pycryptosat', True)
>>> from sage.all import *
>>> from sage.features.sat import Pycryptosat
>>> Pycryptosat().is_present()              # optional - pycryptosat
FeatureTestResult('pycryptosat', True)
sage.features.sat.all_features()[source]