argumentation
Solver rankings on this family, and the generator that reproduces it.
What to run on a problem of this kind
The solvers that did best on this family in the SAT Competition 2026, as images of the companion project. They are a better bet on such a problem than the overall winner of that year, which this family often disagrees with.
| Solver | Solved | Command |
|---|---|---|
| yalun_kissat-eda-1 | 15 / 15 | docker run --rm -v "$PWD:/data" satex/kissat-eda-1:2026 your-instance.cnf |
| biere_kissat-biere | 15 / 15 | no image published for this solver yet |
| yalun_kissat-eda-2 | 15 / 15 | docker run --rm -v "$PWD:/data" satex/kissat-eda-2:2026 your-instance.cnf |
No generator here yet
We have not packaged a generator for this family. If you wrote it, or know where its code lives, a issue is very welcome.
SAT Competition 2023 · 20 instances
Ranked by PAR-2 on this family alone. Winner of the whole main track that year: SBVA-sbva_cadical.
| # | Solver | Solved | PAR-2 per instance | |
|---|---|---|---|---|
| 1 | ReEncode-kissat-ReEncode-pair-kissat.sh | 14 / 20 | 3432 s | |
| 2 | tabularasat-1.0.0 | 14 / 20 | 3474 s | |
| 3 | SBVA-sbva_kissat | 14 / 20 | 3477 s | |
| 4 | AMSAT_ | 14 / 20 | 3529 s | |
| 5 | PReLearn-kissat-PReLearn-kissat.sh | 14 / 20 | 3542 s | |
| 6 | MapleCaDiCaL_LBD-990_275 | 14 / 20 | 3553 s | |
| 7 | MapleCaDiCaL_PPD-950_950 | 14 / 20 | 3576 s | |
| 8 | MapleCaDiCaL_PPD-500_500 | 14 / 20 | 3580 s | |
| 9 | kissat-3.1.0 | 14 / 20 | 3598 s | |
| 10 | MapleCaDiCaL_LBD-990_500 | 14 / 20 | 3642 s | |
| 11 | Cadical_ESA | 14 / 20 | 3648 s | |
| 12 | PReLearn-kissat-PReLearn-tern-kissat.sh | 14 / 20 | 3683 s |
SAT Competition 2024 · 21 instances
Ranked by PAR-2 on this family alone. Winner of the whole main track that year: kissat-sc2024.
| # | Solver | Solved | PAR-2 per instance | |
|---|---|---|---|---|
| 1 | hCaD-pbva | 21 / 21 | 884 s | |
| 2 | kissat-sc2024 | 21 / 21 | 920 s | |
| 3 | hKis-bva | 21 / 21 | 963 s | |
| 4 | hCaD-bva | 21 / 21 | 979 s | |
| 5 | AMSAT | 21 / 21 | 981 s | |
| 6 | AMSAT_RGC | 21 / 21 | 996 s | |
| 7 | CaDiCaL | 21 / 21 | 1118 s | |
| 8 | Cadical_ESA | 21 / 21 | 1183 s | |
| 9 | BreakID-Kissat | 19 / 21 | 1586 s | |
| 10 | Kissat_MAB-DC | 19 / 21 | 2053 s | |
| 11 | Kissat_MAB_ESA | 19 / 21 | 2138 s | |
| 12 | Kissat_MAB_Binary | 19 / 21 | 2139 s |
SAT Competition 2026 · 15 instances
Ranked by PAR-2 on this family alone. Winner of the whole main track that year: anders_satsuma-iter-kissat.
| # | Solver | Solved | PAR-2 per instance | |
|---|---|---|---|---|
| 1 | yalun_kissat-eda-1 | 15 / 15 | 202 s | |
| 2 | biere_kissat-biere | 15 / 15 | 240 s | |
| 3 | yalun_kissat-eda-2 | 15 / 15 | 260 s | |
| 4 | yalun_kissat-eda-3 | 15 / 15 | 262 s | |
| 5 | yalun_kissat-eda-4 | 15 / 15 | 262 s | |
| 6 | guo_kissat-ae-hucb | 15 / 15 | 448 s | |
| 7 | zheng_kissat-mab-hypre | 15 / 15 | 509 s | |
| 8 | zheng_kissat-mab-hypre-v2 | 15 / 15 | 509 s | |
| 9 | liang_kissat-mab-da | 15 / 15 | 641 s | |
| 10 | biere_cadical3 | 15 / 15 | 667 s | |
| 11 | guo_kissat-ae-eg | 14 / 15 | 748 s | |
| 12 | zhenwei_mergesat | 14 / 15 | 755 s |