SAT Heritage - Docker images
Usage
Requirements:
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:
key | type | description |
---|---|---|
name | string | Name of the solver, without case restriction |
call | string | Name of the executable |
path | string | Directory from which the executable should be called. Default: name
|
args | string list | arguments to the executable for simple solving. See below for allowed keywords. |
argsproof | string list | arguments to the executable for solving with proof output. See below for allowed keywords |
gz | boolean | If true, the solver supports natively gzipped input files. If false, an input file ending with .gz will be first decompressed by the wrapper script. |
The following keywords are allowed in args
and argsproof
:
keyword | description |
---|---|
FILECNFÂ | Replaced by the absolute path (within the Docker container) to the input DIMACS file. Whenever the input file ends with .gz and gz is False , the input file is unzipped as /tmp/gunzipped.cnf
|
FILEPOOF | Replaced by the absolute path (within the Docker container) to the output file for proof |
MAXNBTHREAD | Replaced by the MAXNBTHREAD environment variable; 1 by default.Example: satex run asolver:ayear my.cnf -e MAXNBTHREAD=8
|
MEMLIMIT | Replaced by the MEMLIMIT environment variable; 1024 by default. |
TIMEOUT | Replaced by the TIMEOUT environment variable; 3600 by default. |
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.
key | description |
---|---|
base_version | Version of the base image for running the solver available in the base/ directory |
base_from | Image to inherit from for running the solver |
builder | Path to the Docker recipe for compiling the solver. If it is not starting with generic/ , the path is relative to the set directory. The path should contain at least a Dockerfile . The builder recipe should install the solver binaries into /dist . |
builder_base | Image to inherit from for compiling the solver with generic/... builders |
image_name | Python format string with ENTRY being the set name and SOLVER the solver identifier Default: "{SOLVER}:{ENTRY}"
|
dist_version | Version of the recipe for assembling the solver image (generic/dist-{dist_version} )Default: "v1"  |
download_url | Python format string for the downloading the solver source/binary |
BUILD_DEPENDSÂ | Additional packages to install for compiling the solver. Used by generic/v1 builder |
RDEPENDSÂ | Additional packages to install for running the executable. Used by generic/dist-v1 assembler |
Python format strings can use the following variables:
-
SOLVER
: solver identifier (keys insolvers.json
) -
SOLVER_NAME
: solver name (specified insolvers.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}"
}
}