QF_ALIA (Single Query Track)
Competition results for the QF_ALIA
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 176
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| SMTInterpol | SMTInterpol | SMTInterpol | Yices2 | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 170 | 2932.535527 | 2128.888947 | 170 | 98 | 72 | 6 | 0 | 3 | 3 |
| Yices2 | 0 | 162 | 137.662276 | 153.904906 | 162 | 90 | 72 | 14 | 0 | 14 | 0 |
| OpenSMT | 0 | 158 | 5190.596867 | 5207.449583 | 158 | 86 | 72 | 18 | 0 | 18 | 0 |
| cvc5 | 0 | 120 | 18025.2419 | 18040.165171 | 120 | 49 | 71 | 56 | 0 | 56 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 170 | 2932.535527 | 2128.888947 | 170 | 98 | 72 | 6 | 0 | 3 | 3 |
| Yices2 | 0 | 162 | 137.662276 | 153.904906 | 162 | 90 | 72 | 14 | 0 | 14 | 0 |
| OpenSMT | 0 | 158 | 5190.596867 | 5207.449583 | 158 | 86 | 72 | 18 | 0 | 18 | 0 |
| cvc5 | 0 | 120 | 18025.2419 | 18040.165171 | 120 | 49 | 71 | 56 | 0 | 56 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| SMTInterpol | 0 | 98 | 2207.579607 | 1714.642729 | 98 | 98 | 0 | 1 | 77 | 0 | 1 |
| Yices2 | 0 | 90 | 123.992147 | 133.028603 | 90 | 90 | 0 | 9 | 77 | 9 | 0 |
| OpenSMT | 0 | 86 | 4726.867873 | 4736.456656 | 86 | 86 | 0 | 13 | 77 | 13 | 0 |
| cvc5 | 0 | 49 | 15452.100549 | 15459.499141 | 49 | 49 | 0 | 50 | 77 | 50 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 72 | 13.67013 | 20.876304 | 72 | 0 | 72 | 0 | 104 | 0 | 0 |
| SMTInterpol | 0 | 72 | 724.95592 | 414.246217 | 72 | 0 | 72 | 0 | 104 | 0 | 0 |
| OpenSMT | 0 | 72 | 463.728994 | 470.992927 | 72 | 0 | 72 | 0 | 104 | 0 | 0 |
| cvc5 | 0 | 71 | 2573.141351 | 2580.66603 | 71 | 0 | 71 | 1 | 104 | 1 | 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 | 161 | 103.266096 | 119.407557 | 161 | 89 | 72 | 0 | 15 | 0 | 0 |
| SMTInterpol | 0 | 154 | 801.93895 | 322.889147 | 154 | 86 | 68 | 0 | 22 | 0 | 0 |
| OpenSMT | 0 | 120 | 214.747277 | 226.795381 | 120 | 53 | 67 | 0 | 56 | 0 | 0 |
| cvc5 | 0 | 78 | 143.383891 | 151.188748 | 78 | 18 | 60 | 0 | 98 | 0 | 0 |