QF_ABV (Single Query Track)
Competition results for the QF_ABV
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 7574
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Bitwuzla | Bitwuzla | Bitwuzla | Bitwuzla | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 7553 | 17227.347252 | 17986.308626 | 7553 | 5229 | 2324 | 21 | 0 | 19 | 1 |
| Yices2 | 0 | 7538 | 18018.520252 | 18776.306315 | 7538 | 5226 | 2312 | 36 | 0 | 35 | 0 |
| SMTInterpol | 0 | 6442 | 491921.000877 | 421177.429046 | 6447 | 4317 | 2130 | 1127 | 0 | 1038 | 0 |
| cvc5 | 1 | 7440 | 22564.846411 | 23312.005211 | 7441 | 5168 | 2273 | 133 | 0 | 129 | 3 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 7553 | 17227.347252 | 17986.308626 | 7553 | 5229 | 2324 | 21 | 0 | 19 | 1 |
| Yices2 | 0 | 7538 | 18018.520252 | 18776.306315 | 7538 | 5226 | 2312 | 36 | 0 | 35 | 0 |
| SMTInterpol | 0 | 6447 | 498079.307522 | 427067.345705 | 6447 | 4317 | 2130 | 1127 | 0 | 1038 | 0 |
| cvc5 | 1 | 7440 | 22564.846411 | 23312.005211 | 7441 | 5168 | 2273 | 133 | 0 | 129 | 3 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 5229 | 3766.894068 | 4289.79752 | 5229 | 5229 | 0 | 5 | 2340 | 3 | 1 |
| Yices2 | 0 | 5226 | 9248.801356 | 9773.408128 | 5226 | 5226 | 0 | 8 | 2340 | 7 | 0 |
| cvc5 | 0 | 5167 | 14096.502337 | 14615.198471 | 5167 | 5167 | 0 | 67 | 2340 | 63 | 3 |
| SMTInterpol | 0 | 4317 | 366227.169373 | 312126.487411 | 4317 | 4317 | 0 | 917 | 2340 | 830 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 2324 | 13460.453184 | 13696.511107 | 2324 | 0 | 2324 | 16 | 5234 | 16 | 0 |
| Yices2 | 0 | 2312 | 8769.718896 | 9002.898188 | 2312 | 0 | 2312 | 28 | 5234 | 28 | 0 |
| SMTInterpol | 0 | 2130 | 131852.138149 | 114940.858294 | 2130 | 0 | 2130 | 210 | 5234 | 208 | 0 |
| cvc5 | 1 | 2273 | 8468.344074 | 8696.80674 | 2274 | 1 | 2273 | 66 | 5234 | 66 | 0 |
24 seconds Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 7462 | 2040.106953 | 2786.263381 | 7462 | 5181 | 2281 | 1 | 111 | 0 | 0 |
| Bitwuzla | 0 | 7364 | 2117.377584 | 2853.216113 | 7364 | 5204 | 2160 | 1 | 209 | 0 | 0 |
| cvc5 | 0 | 7261 | 5006.444543 | 5731.242928 | 7261 | 5085 | 2176 | 1 | 312 | 0 | 0 |
| SMTInterpol | 0 | 4978 | 27576.002696 | 11305.465008 | 4978 | 3250 | 1728 | 40 | 2556 | 0 | 0 |