hardware-verification
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 |
|---|---|---|
| hKissatInc-unsat | 7 / 8 | docker run --rm -v "$PWD:/data" satex/hkissatinc-unsat:2023 your-instance.cnf |
| hKis-psids | 7 / 8 | docker run --rm -v "$PWD:/data" satex/hkis-psids:2023 your-instance.cnf |
| Kissat_MAB_prop-no_sym | 7 / 8 | no image published for this solver yet |
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 · 8 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 | hKissatInc-unsat | 7 / 8 | 1470 s | |
| 2 | hKis-psids | 7 / 8 | 1491 s | |
| 3 | Kissat_MAB_prop-no_sym | 7 / 8 | 1554 s | |
| 4 | Kissat_MAB_prop_pr-no_sym | 7 / 8 | 1558 s | |
| 5 | Kissat_MAB_Rephases | 7 / 8 | 1560 s | |
| 6 | kissat-hywalk-exp-gb | 7 / 8 | 1561 s | |
| 7 | kissat-hywalk-exp | 7 / 8 | 1562 s | |
| 8 | Kissat_MAB_Conflict | 7 / 8 | 1564 s | |
| 9 | kissat_incsp | 7 / 8 | 1564 s | |
| 10 | kissat-hywalk-gb | 7 / 8 | 1566 s | |
| 11 | Kissat_MAB_Conflict+ | 7 / 8 | 1566 s | |
| 12 | Kissat_MAB_Binary | 7 / 8 | 1575 s |