QF_UFDT (Single Query Track)
Competition results for the QF_UFDT
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 200
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| cvc5 | cvc5 | cvc5 | 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 |
|---|
| cvc5 | 0 | 163 | 50599.046083 | 50633.182017 | 163 | 82 | 81 | 37 | 0 | 37 | 0 |
| Algaroba | 0 | 115 | 27697.077049 | 27716.536118 | 115 | 80 | 35 | 85 | 0 | 85 | 0 |
| Z3-alpha | 0 | 106 | 33284.909706 | 33306.438798 | 106 | 13 | 93 | 94 | 0 | 94 | 0 |
| SMTInterpol | 0 | 36 | 16523.991334 | 11441.069786 | 46 | 21 | 25 | 154 | 0 | 154 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 163 | 50599.046083 | 50633.182017 | 163 | 82 | 81 | 37 | 0 | 37 | 0 |
| Algaroba | 0 | 115 | 27697.077049 | 27716.536118 | 115 | 80 | 35 | 85 | 0 | 85 | 0 |
| Z3-alpha | 0 | 106 | 33284.909706 | 33306.438798 | 106 | 13 | 93 | 94 | 0 | 94 | 0 |
| SMTInterpol | 0 | 46 | 31769.347361 | 19940.47134 | 46 | 21 | 25 | 154 | 0 | 154 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 82 | 8935.75075 | 8947.987509 | 82 | 82 | 0 | 18 | 100 | 18 | 0 |
| Algaroba | 0 | 80 | 5068.09654 | 5078.090843 | 80 | 80 | 0 | 20 | 100 | 20 | 0 |
| SMTInterpol | 0 | 21 | 7169.888512 | 6452.053114 | 21 | 21 | 0 | 79 | 100 | 79 | 0 |
| Z3-alpha | 0 | 13 | 9048.255307 | 9052.281241 | 13 | 13 | 0 | 87 | 100 | 87 | 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 | 93 | 24236.654399 | 24254.157557 | 93 | 0 | 93 | 7 | 100 | 7 | 0 |
| cvc5 | 0 | 81 | 41663.295333 | 41685.194507 | 81 | 0 | 81 | 19 | 100 | 19 | 0 |
| Algaroba | 0 | 35 | 22628.980509 | 22638.445275 | 35 | 0 | 35 | 65 | 100 | 65 | 0 |
| SMTInterpol | 0 | 25 | 24599.458849 | 13488.418226 | 25 | 0 | 25 | 75 | 100 | 75 | 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 | 37 | 411.236014 | 415.159551 | 37 | 37 | 0 | 0 | 163 | 0 | 0 |
| cvc5 | 0 | 16 | 175.49182 | 177.186827 | 16 | 16 | 0 | 0 | 184 | 0 | 0 |
| SMTInterpol | 0 | 4 | 118.482305 | 56.811038 | 4 | 4 | 0 | 0 | 196 | 0 | 0 |
| Z3-alpha | 0 | 3 | 59.217755 | 59.542218 | 3 | 0 | 3 | 0 | 197 | 0 | 0 |