QF_UFIDL (Single Query Track)
Competition results for the QF_UFIDL
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 300
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| OpenSMT | OpenSMT | OpenSMT | OpenSMT | Yices2 |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 276 | 19605.778831 | 19638.548861 | 276 | 101 | 175 | 24 | 0 | 24 | 0 |
| cvc5 | 0 | 243 | 38507.711908 | 38539.716231 | 243 | 86 | 157 | 57 | 0 | 57 | 0 |
| Yices2 | 0 | 237 | 16845.131939 | 16872.860092 | 237 | 67 | 170 | 63 | 0 | 63 | 0 |
| SMTInterpol | 0 | 218 | 17481.457733 | 8718.105322 | 227 | 88 | 139 | 73 | 0 | 73 | 0 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 276 | 19605.778831 | 19638.548861 | 276 | 101 | 175 | 24 | 0 | 24 | 0 |
| cvc5 | 0 | 243 | 38507.711908 | 38539.716231 | 243 | 86 | 157 | 57 | 0 | 57 | 0 |
| Yices2 | 0 | 237 | 16845.131939 | 16872.860092 | 237 | 67 | 170 | 63 | 0 | 63 | 0 |
| SMTInterpol | 0 | 227 | 34642.603173 | 16661.282355 | 227 | 88 | 139 | 73 | 0 | 73 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 101 | 5597.066297 | 5608.918016 | 101 | 101 | 0 | 1 | 198 | 1 | 0 |
| SMTInterpol | 0 | 88 | 18118.62353 | 9007.325901 | 88 | 88 | 0 | 14 | 198 | 14 | 0 |
| cvc5 | 0 | 86 | 17054.732071 | 17066.66539 | 86 | 86 | 0 | 16 | 198 | 16 | 0 |
| Yices2 | 0 | 67 | 8401.21716 | 8410.198782 | 67 | 67 | 0 | 35 | 198 | 35 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| OpenSMT | 0 | 175 | 14008.712534 | 14029.630845 | 175 | 0 | 175 | 23 | 102 | 23 | 0 |
| Yices2 | 0 | 170 | 8443.914779 | 8462.66131 | 170 | 0 | 170 | 28 | 102 | 28 | 0 |
| cvc5 | 0 | 157 | 21452.979837 | 21473.050841 | 157 | 0 | 157 | 41 | 102 | 41 | 0 |
| SMTInterpol | 0 | 139 | 16523.979643 | 7653.956454 | 139 | 0 | 139 | 59 | 102 | 59 | 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 | 197 | 178.254896 | 198.002627 | 197 | 48 | 149 | 0 | 103 | 0 | 0 |
| OpenSMT | 0 | 192 | 923.389209 | 942.833336 | 192 | 68 | 124 | 0 | 108 | 0 | 0 |
| SMTInterpol | 0 | 169 | 2561.994239 | 992.664946 | 169 | 57 | 112 | 0 | 131 | 0 | 0 |
| cvc5 | 0 | 138 | 359.479476 | 373.304575 | 138 | 47 | 91 | 0 | 162 | 0 | 0 |