lymphosat
Awards
- 1st SAT · AI generated / AI tuned subtrack 2026 source
Notes
Winner of the AI generated / AI tuned subtrack (SAT category). Composite solver (126 family-specific solvers and a Kissat-based fallback) selected at run time by the submitted dispatcher; built with the authors' portable generic-build.sh for the dispatcher and the fallback. The family-specific solvers keep the authors' -march=icelake-server flags (some use AVX-512 intrinsics and do not compile otherwise), so on a CPU without AVX-512 the families they cover fail with an illegal instruction and the dispatcher falls back to the Kissat-based fallback, compiled here for generic x86-64 (CC overridden) so that the image answers on any machine. The proof is VeriPB, which satex cannot check, so no argsproof.
Licence
permissive You can use it, modify it and ship it in your own software, commercial or not, as long as you keep the copyright notices.
- 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 lymphosat/src/solver/solvers/fallback/solver/src/LICENSE; this summary is informative, the licence text prevails. Corrections welcome by pull request.
Pull it from Docker and run it
docker pull satex/lymphosat:2026 docker run --rm -v $PWD:/data satex/lymphosat: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 lymphosat:2026 rebuilds the same image on your own machine if you would rather not trust ours (slower, same solver).
Download the sources lymphosat.tar.xz, the competition submission as archived by SAT Heritage, to build it yourself with the recipe below. Downloaded 7 times.
- Licence
- MIT (licence file lymphosat/src/solver/solvers/fallback/solver/src/LICENSE)
- Image
satex/lymphosat:2026- Command
bash 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
export CC="gcc -march=x86-64-v2 -mtune=generic -fomit-frame-pointer"; rm -rf solver/.build solver/.build-generic && bash ./generic-build.sh- Build dependencies
- clang lld cmake python3
- Runtime dependencies
- python3
- Sources
- lymphosat.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 |