QF_UF (Single Query Track)
Competition results for the QF_UF
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 3521
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 | 3521 | 1414.320688 | 1767.470129 | 3521 | 1450 | 2071 | 0 | 0 | 0 | 0 |
| Z3-alpha | 0 | 3521 | 3503.547518 | 3856.312824 | 3521 | 1450 | 2071 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 3520 | 6183.099754 | 6536.194407 | 3520 | 1450 | 2070 | 1 | 0 | 1 | 0 |
| OpenSMT | 0 | 3520 | 6626.809537 | 6982.161915 | 3520 | 1450 | 2070 | 1 | 0 | 1 | 0 |
| plat-smt | 0 | 3512 | 6743.388633 | 7096.204421 | 3512 | 1450 | 2062 | 9 | 0 | 9 | 0 |
| SMTInterpol | 0 | 3443 | 30567.814223 | 13260.396322 | 3459 | 1450 | 2009 | 62 | 0 | 60 | 0 |
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 | 3521 | 1414.320688 | 1767.470129 | 3521 | 1450 | 2071 | 0 | 0 | 0 | 0 |
| Z3-alpha | 0 | 3521 | 3503.547518 | 3856.312824 | 3521 | 1450 | 2071 | 0 | 0 | 0 | 0 |
| cvc5 | 0 | 3520 | 6183.099754 | 6536.194407 | 3520 | 1450 | 2070 | 1 | 0 | 1 | 0 |
| OpenSMT | 0 | 3520 | 6626.809537 | 6982.161915 | 3520 | 1450 | 2070 | 1 | 0 | 1 | 0 |
| plat-smt | 0 | 3512 | 6743.388633 | 7096.204421 | 3512 | 1450 | 2062 | 9 | 0 | 9 | 0 |
| SMTInterpol | 0 | 3459 | 62882.743861 | 26844.980758 | 3459 | 1450 | 2009 | 62 | 0 | 60 | 0 |
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 | 1450 | 220.090789 | 365.384617 | 1450 | 1450 | 0 | 0 | 2071 | 0 | 0 |
| plat-smt | 0 | 1450 | 302.089867 | 447.218875 | 1450 | 1450 | 0 | 0 | 2071 | 0 | 0 |
| OpenSMT | 0 | 1450 | 363.894721 | 509.518687 | 1450 | 1450 | 0 | 0 | 2071 | 0 | 0 |
| Z3-alpha | 0 | 1450 | 379.830369 | 524.900342 | 1450 | 1450 | 0 | 0 | 2071 | 0 | 0 |
| cvc5 | 0 | 1450 | 472.950242 | 617.887643 | 1450 | 1450 | 0 | 0 | 2071 | 0 | 0 |
| SMTInterpol | 0 | 1450 | 4087.286919 | 1704.066182 | 1450 | 1450 | 0 | 0 | 2071 | 0 | 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 | 2071 | 1194.229899 | 1402.085511 | 2071 | 0 | 2071 | 0 | 1450 | 0 | 0 |
| Z3-alpha | 0 | 2071 | 3123.717149 | 3331.412482 | 2071 | 0 | 2071 | 0 | 1450 | 0 | 0 |
| cvc5 | 0 | 2070 | 5710.149512 | 5918.306764 | 2070 | 0 | 2070 | 1 | 1450 | 1 | 0 |
| OpenSMT | 0 | 2070 | 6262.914816 | 6472.643229 | 2070 | 0 | 2070 | 1 | 1450 | 1 | 0 |
| plat-smt | 0 | 2062 | 6441.298766 | 6648.985546 | 2062 | 0 | 2062 | 9 | 1450 | 9 | 0 |
| SMTInterpol | 0 | 2009 | 58795.456941 | 25140.914576 | 2009 | 0 | 2009 | 62 | 1450 | 60 | 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 | 3520 | 633.953398 | 986.708941 | 3520 | 1450 | 2070 | 0 | 1 | 0 | 0 |
| Z3-alpha | 0 | 3501 | 1845.219568 | 2195.734902 | 3501 | 1450 | 2051 | 0 | 20 | 0 | 0 |
| OpenSMT | 0 | 3486 | 2036.176418 | 2386.674137 | 3486 | 1450 | 2036 | 0 | 35 | 0 | 0 |
| cvc5 | 0 | 3482 | 1784.564836 | 2132.739689 | 3482 | 1450 | 2032 | 0 | 39 | 0 | 0 |
| plat-smt | 0 | 3473 | 1296.137595 | 1643.942785 | 3473 | 1450 | 2023 | 0 | 48 | 0 | 0 |
| SMTInterpol | 0 | 3400 | 22965.48686 | 9380.559384 | 3400 | 1450 | 1950 | 0 | 121 | 0 | 0 |