QF_RDL (Single Query Track)
Competition results for the QF_RDL
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 247
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Yices2 | Yices2 | Yices2 | 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 |
|---|
| Yices2 | 0 | 213 | 1516.670976 | 1538.324036 | 213 | 105 | 108 | 34 | 0 | 34 | 0 |
| cvc5 | 0 | 209 | 7043.085978 | 7065.231082 | 209 | 102 | 107 | 38 | 0 | 38 | 0 |
| Z3-alpha | 0 | 207 | 4848.43094 | 4870.300382 | 207 | 99 | 108 | 40 | 0 | 21 | 0 |
| OpenSMT | 0 | 194 | 13818.132006 | 13840.012458 | 194 | 100 | 94 | 53 | 0 | 53 | 0 |
| SMTInterpol | 0 | 182 | 12690.007503 | 9130.458073 | 182 | 101 | 81 | 65 | 0 | 63 | 2 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 213 | 1516.670976 | 1538.324036 | 213 | 105 | 108 | 34 | 0 | 34 | 0 |
| cvc5 | 0 | 209 | 7043.085978 | 7065.231082 | 209 | 102 | 107 | 38 | 0 | 38 | 0 |
| Z3-alpha | 0 | 207 | 4848.43094 | 4870.300382 | 207 | 99 | 108 | 40 | 0 | 21 | 0 |
| OpenSMT | 0 | 194 | 13818.132006 | 13840.012458 | 194 | 100 | 94 | 53 | 0 | 53 | 0 |
| SMTInterpol | 0 | 182 | 12690.007503 | 9130.458073 | 182 | 101 | 81 | 65 | 0 | 63 | 2 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Yices2 | 0 | 105 | 382.091138 | 392.718783 | 105 | 105 | 0 | 0 | 142 | 0 | 0 |
| cvc5 | 0 | 102 | 2712.421347 | 2723.133431 | 102 | 102 | 0 | 3 | 142 | 3 | 0 |
| SMTInterpol | 0 | 101 | 6510.206189 | 5484.208978 | 101 | 101 | 0 | 4 | 142 | 4 | 0 |
| OpenSMT | 0 | 100 | 7182.079148 | 7193.037628 | 100 | 100 | 0 | 5 | 142 | 5 | 0 |
| Z3-alpha | 0 | 99 | 2854.65979 | 2865.353278 | 99 | 99 | 0 | 6 | 142 | 6 | 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 | 108 | 1134.579838 | 1145.605252 | 108 | 0 | 108 | 1 | 138 | 1 | 0 |
| Z3-alpha | 0 | 108 | 1993.77115 | 2004.947104 | 108 | 0 | 108 | 1 | 138 | 1 | 0 |
| cvc5 | 0 | 107 | 4330.66463 | 4342.097652 | 107 | 0 | 107 | 2 | 138 | 2 | 0 |
| OpenSMT | 0 | 94 | 6636.052858 | 6646.97483 | 94 | 0 | 94 | 15 | 138 | 15 | 0 |
| SMTInterpol | 0 | 81 | 6179.801314 | 3646.249095 | 81 | 0 | 81 | 28 | 138 | 26 | 2 |
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 | 195 | 338.848689 | 358.413923 | 195 | 99 | 96 | 0 | 52 | 0 | 0 |
| Z3-alpha | 0 | 183 | 517.408434 | 535.834371 | 183 | 90 | 93 | 19 | 45 | 0 | 0 |
| cvc5 | 0 | 170 | 586.721044 | 603.869152 | 170 | 88 | 82 | 0 | 77 | 0 | 0 |
| OpenSMT | 0 | 147 | 358.772855 | 373.676139 | 147 | 80 | 67 | 0 | 100 | 0 | 0 |
| SMTInterpol | 0 | 136 | 1750.87111 | 769.57128 | 136 | 75 | 61 | 0 | 111 | 0 | 0 |