SAT Heritage - Docker images of SAT solvers

A community-driven effort for archiving, building and running more than thousand SAT solvers

Principles

SAT research has a long history of source code and binary releases, thanks to competitions organized every year. However, since every cycle of competitions has its own set of rules and an adhoc way of publishing source code and binaries, compiling or even running any solver may be harder than what it seems. And there has been more than a thousand solvers published so far, some of them released in the early 90's!

This project drives a community-driven effort to archive and to allow easy compilation and running of all SAT solvers that have been released so far.

Thanks to our tool, building (or running) a solver from its source (or from its binary) can be done in one line.

Usage

Requirements:

• Docker

docker run --rm -v $PWD:/data satex/<tool>:<year> <DIMACS> [<PROOF>]

satex Python script

Requirements:

• Python ≥3.6
• Docker

pip install -U satex     # you may have to use pip3

In case satex commands fails with command not found error, try doing export PATH=$HOME/.local/bin:$PATH beforehand. If it works, add this fixture within your ~/.bashrc or ~/.profile file. See https://packaging.python.org/tutorials/installing-packages/#installing-to-the-user-site

List images

satex list
satex list '*:2018'
satex list 'maple*'

By default, satex considers only solvers which have been validated. Solvers which are not yet validated can be listed with --unstable option; those which are not compiling/working with --fixme; all the referenced solvers are considered with the --all option:

satex list --fixme      # solvers to be fixed
satex list --unstable   # solvers to be tested
satex list --all        # all referenced solvers

Information

Print information related to solvers, including authors, command line, validation status. and possibly comments.

satex info 'glucose*'
satex info '*:2018'

Run images

satex run cadical:2019 dimacs [proof]
satex run '*:2016' dimacs [proof]
satex run '*:2009' dimacs -e MAXNBTHREAD=24

Run images with direct call to solvers

satex run-raw cadical:2019 -h

Open shell

satex shell cadical:2019

Extract solvers binaries

satex extract '*:2019' /tmp/

Repository management

Usage:

satex build '*:2018'
satex test '*:2018'
satex push '*:2018'

Persistent storage for sources and binaries

Consider using Zenodo for storing your software, as it provides persistent and versioned URLs.

See https://zenodo.org/communities/satex.

Adding solvers

Solvers are grouped by sets, typically year of competitions. Each set has its own directory and is referenced in index.json. The minimal structure of a <set> directory is the following:

• <set>/solvers.json: configuration file for running solvers.
• <set>/setup.json: configuration file for building images

solvers.json

JSON object where keys are the solver identifiers (necessarily in lower case), and values are JSON objects with the following keys:

The following keywords are allowed in args and argsproof:

Example

{
    "abcdsat": {
        "name": "abcdSAT_drup",
        "call": "./abcdsat_drup",
        "gz": true,
        "args": [
          "FILECNF"
        ],
        "argsproof": [
          "FILECNF",
          "-certified",
          "-certified-output=FILEPROOF"
        ]
    },
    "lingeling": {
        "call": "./lingeling",
        "name": "Lingelingbbcmain",
        "gz": true,
        "args": [
          "FILECNF"
        ],
        "argsproof": [
          "FILECNF",
          "-t",
          "FILEPROOF"
        ]
    }
}

setup.json

JSON object with the following keys, used by default for each solver. A solver can override these by adding a key with its identifier and a value being a JSON object with a subset of the following keys.

Python format strings can use the following variables:

• SOLVER: solver identifier (keys in solvers.json)
• SOLVER_NAME: solver name (specified in solvers.json)

The images for running and building the solver (base_from and builder_base) are usually Debian distribution of the year of the competition: see debian and debian/eol DockerHub repositories, and timeline and detailed history of Debian releases.

Example:

{
    "base_version": "v1",
    "base_from": "debian:stretch-slim",
    "builder": "generic/v1",
    "builder_base": "debian:stretch-slim",
    "download_url": "https://zenodo.org/record/abcdef/files/{SOLVER_NAME}.zip?download=1",
    "asolver": {
        "builder": "generic/binary-v1",
        "download_url": "https://github.com/sat-heritage/docker-images/releases/download/packages/{SOLVER_NAME}"
    }
}

License

The Docker images are for academic and educational use only.

The satex (satex.py) program is distributed under the MIT license. Please see the LICENSE file for more details.