QF_DT (Single Query Track)
Competition results for the QF_DT
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 352
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Algaroba | Algaroba | Algaroba | Z3-alpha | Algaroba |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Algaroba | 0 | 218 | 28127.432787 | 28158.761488 | 218 | 40 | 178 | 134 | 0 | 134 | 0 |
| Z3-alpha | 0 | 216 | 57267.747165 | 57307.764638 | 216 | 25 | 191 | 136 | 0 | 136 | 0 |
| SMTInterpol | 0 | 163 | 25022.31386 | 14309.049261 | 175 | 10 | 165 | 177 | 0 | 175 | 2 |
| cvc5 | 0 | 163 | 31248.585574 | 31275.452207 | 163 | 40 | 123 | 189 | 0 | 189 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Algaroba | 0 | 218 | 28127.432787 | 28158.761488 | 218 | 40 | 178 | 134 | 0 | 134 | 0 |
| Z3-alpha | 0 | 216 | 57267.747165 | 57307.764638 | 216 | 25 | 191 | 136 | 0 | 136 | 0 |
| SMTInterpol | 0 | 175 | 46665.020098 | 26051.733693 | 175 | 10 | 165 | 177 | 0 | 175 | 2 |
| cvc5 | 0 | 163 | 31248.585574 | 31275.452207 | 163 | 40 | 123 | 189 | 0 | 189 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Algaroba | 0 | 40 | 3000.359384 | 3005.226855 | 40 | 40 | 0 | 9 | 303 | 9 | 0 |
| cvc5 | 0 | 40 | 6516.375043 | 6522.67622 | 40 | 40 | 0 | 9 | 303 | 9 | 0 |
| Z3-alpha | 0 | 25 | 14032.62438 | 14039.985511 | 25 | 25 | 0 | 24 | 303 | 24 | 0 |
| SMTInterpol | 0 | 10 | 2334.602755 | 1407.665059 | 10 | 10 | 0 | 39 | 303 | 39 | 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-alpha | 0 | 191 | 43235.122784 | 43267.779126 | 191 | 0 | 191 | 38 | 123 | 38 | 0 |
| Algaroba | 0 | 178 | 25127.073404 | 25153.534633 | 178 | 0 | 178 | 51 | 123 | 51 | 0 |
| SMTInterpol | 0 | 165 | 44330.417343 | 24644.068633 | 165 | 0 | 165 | 64 | 123 | 62 | 2 |
| cvc5 | 0 | 123 | 24732.210531 | 24752.775987 | 123 | 0 | 123 | 106 | 123 | 106 | 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 |
|---|
| Algaroba | 0 | 129 | 479.066349 | 492.302619 | 129 | 19 | 110 | 0 | 223 | 0 | 0 |
| SMTInterpol | 0 | 104 | 931.804468 | 383.604531 | 104 | 6 | 98 | 0 | 248 | 0 | 0 |
| Z3-alpha | 0 | 86 | 167.31403 | 176.056295 | 86 | 3 | 83 | 0 | 266 | 0 | 0 |
| cvc5 | 0 | 81 | 196.459893 | 204.697319 | 81 | 12 | 69 | 0 | 271 | 0 | 0 |