scheduling
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 |
|---|---|---|
| AMSAT | 35 / 50 | docker run --rm -v "$PWD:/data" satex/amsat:2024 your-instance.cnf |
| AMSAT_RGC | 34 / 50 | docker run --rm -v "$PWD:/data" satex/amsat-rgc:2024 your-instance.cnf |
| Kissat_MAB-DC | 32 / 50 | docker run --rm -v "$PWD:/data" satex/kissat-mab-dc:2024 your-instance.cnf |
Generator: Round-robin tournament scheduling
rr-gen rr TEAMS ROUNDS | rr-gen mv TEAMS ROUNDS VENUES
20 of 20 instances of this family regenerated exactly. Details and commands.
SAT Competition 2024 · 50 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 | AMSAT | 35 / 50 | 3578 s | |
| 2 | AMSAT_RGC | 34 / 50 | 3707 s | |
| 3 | Kissat_MAB-DC | 32 / 50 | 3961 s | |
| 4 | hKis-bva | 32 / 50 | 3974 s | |
| 5 | Kissat_MAB_Binary | 31 / 50 | 4086 s | |
| 6 | Kissat_MAB_ESA | 31 / 50 | 4163 s | |
| 7 | kissat-sc2024 | 30 / 50 | 4235 s | |
| 8 | hCaD-bva | 31 / 50 | 4381 s | |
| 9 | CaDiCaL | 29 / 50 | 4448 s | |
| 10 | Cadical_ESA | 29 / 50 | 4510 s | |
| 11 | BreakID-Kissat | 29 / 50 | 4515 s | |
| 12 | hCaD-pbva | 28 / 50 | 4909 s |