cryptography
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 2024, 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 |
|---|---|---|
| Kissat_MAB_ESA | 8 / 9 | docker run --rm -v "$PWD:/data" satex/kissat-mab-esa:2024 your-instance.cnf |
| Kissat_MAB_Binary | 8 / 9 | docker run --rm -v "$PWD:/data" satex/kissat-mab-binary:2024 your-instance.cnf |
| AMSAT_RGC | 8 / 9 | docker run --rm -v "$PWD:/data" satex/amsat-rgc:2024 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 2024 · 9 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 | Kissat_MAB_ESA | 8 / 9 | 1353 s | |
| 2 | Kissat_MAB_Binary | 8 / 9 | 1476 s | |
| 3 | AMSAT_RGC | 8 / 9 | 1594 s | |
| 4 | AMSAT | 8 / 9 | 1615 s | |
| 5 | kissat-sc2024 | 8 / 9 | 1637 s | |
| 6 | Kissat_MAB-DC | 8 / 9 | 1676 s | |
| 7 | hKis-bva | 7 / 9 | 2446 s | |
| 8 | BreakID-Kissat | 7 / 9 | 2483 s | |
| 9 | Cadical_ESA | 7 / 9 | 2852 s | |
| 10 | hCaD-pbva | 7 / 9 | 3012 s | |
| 11 | CaDiCaL | 7 / 9 | 3367 s | |
| 12 | hCaD-bva | 6 / 9 | 3839 s |