brent-equations
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 2023, 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 |
|---|---|---|
| Cadical_rel_1.5.3.Scavel | 19 / 19 | no image published for this solver yet |
| MapleCaDiCaL_LBD-990_500 | 19 / 19 | docker run --rm -v "$PWD:/data" satex/maplecadical-lbd-990-500:2023 your-instance.cnf |
| MapleCaDiCaL_PPD-950_950 | 19 / 19 | docker run --rm -v "$PWD:/data" satex/maplecadical-ppd-950-950:2023 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 · 19 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 | Cadical_rel_1.5.3.Scavel | 19 / 19 | 154 s | |
| 2 | MapleCaDiCaL_LBD-990_500 | 19 / 19 | 155 s | |
| 3 | MapleCaDiCaL_PPD-950_950 | 19 / 19 | 174 s | |
| 4 | CaDiCaL_vivinst | 19 / 19 | 176 s | |
| 5 | Cadical_ESA | 19 / 19 | 184 s | |
| 6 | MapleCaDiCaL_PPD-500_500 | 19 / 19 | 190 s | |
| 7 | hKis-unsat | 19 / 19 | 196 s | |
| 8 | MapleCaDiCaL_LBD-990_275 | 19 / 19 | 204 s | |
| 9 | SBVA-sbva_cadical | 19 / 19 | 233 s | |
| 10 | kissat-3.1.0 | 19 / 19 | 250 s | |
| 11 | Kissat_MAB_Conflict+ | 19 / 19 | 284 s | |
| 12 | Kissat_MAB_Rephases | 19 / 19 | 285 s |