QF_S (Single Query Track)
Competition results for the QF_S
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 8867
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| Z3-Noodler | Z3-Noodler | Z3-Noodler | Z3-Noodler | Z3-Noodler |
Sequential Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-Noodler | 0 | 8853 | 2660.876297 | 3547.170012 | 8853 | 5825 | 3028 | 14 | 0 | 6 | 8 |
| cvc5 | 0 | 8818 | 28789.31133 | 29675.403331 | 8818 | 5816 | 3002 | 49 | 0 | 45 | 4 |
| OSTRICH | 0 | 8813 | 33846.235811 | 19091.558809 | 8822 | 5796 | 3026 | 45 | 0 | 45 | 0 |
| Z3-alpha | 0 | 8810 | 67238.271114 | 68132.883326 | 8810 | 5814 | 2996 | 57 | 0 | 43 | 4 |
Parallel Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-Noodler | 0 | 8853 | 2660.876297 | 3547.170012 | 8853 | 5825 | 3028 | 14 | 0 | 6 | 8 |
| OSTRICH | 0 | 8822 | 53932.915098 | 25957.730625 | 8822 | 5796 | 3026 | 45 | 0 | 45 | 0 |
| cvc5 | 0 | 8818 | 28789.31133 | 29675.403331 | 8818 | 5816 | 3002 | 49 | 0 | 45 | 4 |
| Z3-alpha | 0 | 8810 | 67238.271114 | 68132.883326 | 8810 | 5814 | 2996 | 57 | 0 | 43 | 4 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-Noodler | 0 | 5825 | 1729.253665 | 2312.421066 | 5825 | 5825 | 0 | 0 | 3042 | 0 | 0 |
| cvc5 | 0 | 5816 | 8319.688187 | 8901.140114 | 5816 | 5816 | 0 | 9 | 3042 | 7 | 2 |
| Z3-alpha | 0 | 5814 | 49978.193316 | 50571.186868 | 5814 | 5814 | 0 | 11 | 3042 | 5 | 1 |
| OSTRICH | 0 | 5796 | 44383.395285 | 19900.183629 | 5796 | 5796 | 0 | 29 | 3042 | 29 | 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-Noodler | 0 | 3028 | 931.622632 | 1234.748946 | 3028 | 0 | 3028 | 5 | 5834 | 3 | 2 |
| OSTRICH | 0 | 3026 | 9549.519812 | 6057.546996 | 3026 | 0 | 3026 | 7 | 5834 | 7 | 0 |
| cvc5 | 0 | 3002 | 20469.623143 | 20774.263218 | 3002 | 0 | 3002 | 31 | 5834 | 29 | 2 |
| Z3-alpha | 0 | 2996 | 17260.077799 | 17561.696458 | 2996 | 0 | 2996 | 37 | 5834 | 32 | 3 |
24 seconds Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Z3-Noodler | 0 | 8850 | 1663.145647 | 2548.821968 | 8850 | 5823 | 3027 | 0 | 17 | 0 | 0 |
| OSTRICH | 0 | 8778 | 26192.579717 | 13932.168118 | 8778 | 5758 | 3020 | 0 | 89 | 0 | 0 |
| cvc5 | 0 | 8731 | 1906.503459 | 2777.245502 | 8731 | 5787 | 2944 | 0 | 136 | 0 | 0 |
| Z3-alpha | 0 | 8722 | 3004.575524 | 3878.470851 | 8722 | 5753 | 2969 | 0 | 145 | 0 | 0 |