satsuma-iter-kissat
Notes
Competition name: satsuma-iter+kissat, winner of the main track. Satsuma symmetry breaking (satsuma fix --bsr) followed by the solver, driven by the submitted original-run.sh; the proof is in the SR format, which satex cannot check, so no argsproof. Satsuma's -march=native replaced by a generic x86-64 target so that the image runs on any machine.
Licence
copyleft (GPL) Components under different licences: the strictest one rules the whole. You can use and modify it freely, but a program you redistribute with this solver inside must be GPL too, with its sources.
- GNU General Public License 2.0 GPL-2.0 · copyleft (GPL)
Any program that includes or links this code and is redistributed must be released under the GPL, sources included. Free to use and modify otherwise. Full text - GNU General Public License 3.0 GPL-3.0 · copyleft (GPL)
Any program that includes or links this code and is redistributed must be released under the GPL, sources included. Free to use and modify otherwise. Full text - MIT License MIT · permissive
Use, modify and redistribute freely, in source or binary form, as long as the copyright notice and the licence text stay with the code. This is MiniSat's licence, inherited by most of its descendants. Full text
Read from licence file satsuma-iter-kissat/src/solver/satsuma-dev/src/cliquer/LICENSE, satsuma-iter-kissat/src/LICENSE, satsuma-iter-kissat/src/solver/AE_kissat2025_MAB/LICENSE; this summary is informative, the licence text prevails. Corrections welcome by pull request.
Pull it from Docker and run it
docker pull satex/satsuma-iter-kissat:2026 docker run --rm -v $PWD:/data satex/satsuma-iter-kissat:2026 instance.cnf
No build needed: the image is published on Docker Hub (checked 2026-09-25). Mount the directory that holds your instance on /data; the proof file is optional and not produced by this solver. Its full provenance is kept: the archived sources, the pinned build environment and the recipe are all listed below, and satex build satsuma-iter-kissat:2026 rebuilds the same image on your own machine if you would rather not trust ours (slower, same solver).
Download the sources satsuma-iter-kissat.tar.xz, the competition submission as archived by SAT Heritage, to build it yourself with the recipe below. Downloaded 7 times.
- Licence
- GPL-2.0, GPL-3.0, MIT (licence file satsuma-iter-kissat/src/solver/satsuma-dev/src/cliquer/LICENSE, satsuma-iter-kissat/src/LICENSE, satsuma-iter-kissat/src/solver/AE_kissat2025_MAB/LICENSE)
- Image
satex/satsuma-iter-kissat:2026- Command
bash original-run.sh FILECNF PROOFDIR- Compressed input
- decompressed by the image
- Competition
- SAT Competition 2026
How it is built
- Recipe
- submitted build script
- Builder
generic/starexec-v2- Environment
debian:trixie-20260623-slim@sha256:28de0877c2189802884ccd20f15ee41c203573bd87bb6b883f5f46362d24c5c2· APT snapshot 20260623T000000Z- Build command
grep -rl -e -march=native --include=Makefile --include=makefile --include=CMakeLists.txt . | xargs -r sed -i 's/-march=native/-march=x86-64-v2/g'; bash ./build.sh- Sources
- satsuma-iter-kissat.tar.xz
Last verification
Run on 2026-09-16.
Build
| build-environment | ok | |
| builder-base-image | ok | |
| compile | ok | |
| docker-engine | ok | |
| image-assemble | ok | |
| runtime-base | ok | |
| runtime-base-image | ok | |
| runtime-dependencies | ok | |
| source-download | ok | |
| source-extract | ok |
Tests
| launch | ok | |
| sat-gzip-model | ok | |
| sat-gzip-result | ok | SAT |
| sat-gzip-termination | ok | SAT |
| sat-model | ok | |
| sat-result | ok | SAT |
| sat-termination | ok | SAT |
| unsat-proof | skip | unsupported |
| unsat-result | ok | UNSAT |
| unsat-termination | ok | UNSAT |