QF_SLIA (Single Query Track)
Competition results for the QF_SLIA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 23722
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Z3-Noodler | Z3-Noodler | Z3-Noodler | Z3-Noodler | Z3-Noodler |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-Noodler | 0 | 23272 | 27133.73947 | 29468.738828 | 23272 | 15470 | 7802 | 446 | 4 | 200 | 11 |
| cvc5 | 0 | 21569 | 795526.095248 | 797863.604368 | 21569 | 14129 | 7440 | 2149 | 4 | 2145 | 0 |
| Z3-alpha | 0 | 20767 | 381710.546885 | 383866.16311 | 20767 | 13092 | 7675 | 2951 | 4 | 2515 | 45 |
| OSTRICH | 0 | 20448 | 593929.119032 | 316872.610053 | 20499 | 12788 | 7711 | 3219 | 4 | 3218 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-Noodler | 0 | 23272 | 27133.73947 | 29468.738828 | 23272 | 15470 | 7802 | 446 | 4 | 200 | 11 |
| cvc5 | 0 | 21569 | 795526.095248 | 797863.604368 | 21569 | 14129 | 7440 | 2149 | 4 | 2145 | 0 |
| Z3-alpha | 0 | 20767 | 381710.546885 | 383866.16311 | 20767 | 13092 | 7675 | 2951 | 4 | 2515 | 45 |
| OSTRICH | 0 | 20499 | 676314.990431 | 363433.916434 | 20499 | 12788 | 7711 | 3219 | 4 | 3218 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-Noodler | 0 | 15470 | 16457.774124 | 18009.818636 | 15470 | 15470 | 0 | 253 | 7999 | 158 | 7 |
| cvc5 | 0 | 14129 | 716050.039734 | 717629.927043 | 14129 | 14129 | 0 | 1594 | 7999 | 1594 | 0 |
| Z3-alpha | 0 | 13092 | 253367.645564 | 254731.392307 | 13092 | 13092 | 0 | 2631 | 7999 | 2324 | 28 |
| OSTRICH | 0 | 12788 | 546460.820814 | 288859.51803 | 12788 | 12788 | 0 | 2935 | 7999 | 2934 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-Noodler | 0 | 7802 | 10675.965345 | 11458.920192 | 7802 | 0 | 7802 | 171 | 15749 | 41 | 3 |
| OSTRICH | 0 | 7711 | 129854.169617 | 74574.398403 | 7711 | 0 | 7711 | 262 | 15749 | 262 | 0 |
| Z3-alpha | 0 | 7675 | 128342.901321 | 129134.770803 | 7675 | 0 | 7675 | 298 | 15749 | 190 | 17 |
| cvc5 | 0 | 7440 | 79476.055514 | 80233.677325 | 7440 | 0 | 7440 | 533 | 15749 | 529 | 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 |
|---|
| Z3-Noodler | 0 | 23187 | 9687.439161 | 12009.38336 | 23187 | 15421 | 7766 | 235 | 300 | 0 | 0 |
| Z3-alpha | 0 | 19692 | 17373.214882 | 19350.086103 | 19692 | 12174 | 7518 | 97 | 3933 | 0 | 0 |
| cvc5 | 0 | 19227 | 11209.357276 | 13129.131852 | 19227 | 12064 | 7163 | 4 | 4491 | 0 | 0 |
| OSTRICH | 0 | 18770 | 247254.296015 | 99116.305597 | 18770 | 11316 | 7454 | 0 | 4952 | 0 | 0 |