sagemath_kissat: Interface to the SAT solver kissat

This pip-installable distribution passagemath-kissat provides an interface to the SAT solver kissat, a condensed and improved reimplementation of CaDiCaL in C.

What is included

  • Binary wheels on PyPI contain prebuilt copies of the kissat executable.

Examples

Using kissat programs on the command line:

$ pipx run --pip-args="--prefer-binary" --spec "passagemath-kissat" sage -sh -c kissat

Finding the installation location of the kissat program:

$ pipx run --pip-args="--prefer-binary" --spec "passagemath-kissat[test]" ipython

In [1]: from sage.features.sat import Kissat

In [2]: Kissat().absolute_filename()
Out[2]: '.../bin/kissat'

Use with sage.sat:

$ pipx run --pip-args="--prefer-binary" --spec "passagemath-kissat[test]" ipython

In [1]: from sage.all__sagemath_kissat import *

In [2]: from sage.sat.solvers.dimacs import Kissat

In [3]: solver = Kissat(); solver.add_clause((1,2)); solver.add_clause((-1,2)); solver.add_clause((1,-2))

In [4]: solver()
Out[4]: (None, True, True)

Type

optional

Dependencies

Version Information

package-version.txt:

10.6.29

version_requirements.txt:

passagemath-kissat ~= 10.6.29.0

Installation commands

$ pip install passagemath-kissat~=10.6.29.0
$ sage -i sagemath_kissat

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