allowable-seqence
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 |
|---|---|---|
| oertel_satsuma-lex-ae-kissat-mab | 14 / 16 | docker run --rm -v "$PWD:/data" satex/satsuma-lex-ae-kissat-mab:2026 your-instance.cnf |
| zheng_kissat-mab-hypre | 13 / 16 | docker run --rm -v "$PWD:/data" satex/kissat-mab-hypre:2026 your-instance.cnf |
| zheng_kissat-mab-hypre-v2 | 13 / 16 | docker run --rm -v "$PWD:/data" satex/kissat-mab-hypre-v2: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 2026 · 16 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 | oertel_satsuma-lex-ae-kissat-mab | 14 / 16 | 2671 s | |
| 2 | zheng_kissat-mab-hypre | 13 / 16 | 2929 s | |
| 3 | zheng_kissat-mab-hypre-v2 | 13 / 16 | 2931 s | |
| 4 | anders_satsuma-iter-ae-kissat-mab | 13 / 16 | 3109 s | |
| 5 | biere_kissat-biere | 13 / 16 | 3220 s | |
| 6 | yalun_kissat-eda-2 | 13 / 16 | 3307 s | |
| 7 | yalun_kissat-eda-3 | 13 / 16 | 3314 s | |
| 8 | guo_kissat-ae-eg | 12 / 16 | 3405 s | |
| 9 | oertel_satsuma-lex-kissat | 12 / 16 | 3432 s | |
| 10 | guo_kissat-ae-hucb | 12 / 16 | 3477 s | |
| 11 | anders_satsuma-iter-kissat | 12 / 16 | 3617 s | |
| 12 | liang_kissat-mab-da | 12 / 16 | 3714 s |