SAT Heritage - Docker images

Usage

Requirements:

• Docker

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

satex Python script

Python >= 3 is required.

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

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 Debian version history.

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}"
    }
}