QF_Strings (Single Query Track)
Competition results for the QF_Strings
division
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 32659
Time Limit: 1200 seconds
Memory Limit: 20480 GB
Logics: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 | 32195 | 29805.069455 | 33033.36176 | 32195 | 21365 | 10830 | 460 | 4 | 206 | 19 |
| cvc5 | 0 | 30457 | 824325.113303 | 827555.717045 | 30457 | 20015 | 10442 | 2198 | 4 | 2190 | 4 |
| Z3-alpha | 0 | 29647 | 448961.923086 | 452019.222369 | 29647 | 18976 | 10671 | 3008 | 4 | 2558 | 49 |
| OSTRICH | 0 | 29331 | 628004.79958 | 336081.853711 | 29391 | 18654 | 10737 | 3264 | 4 | 3263 | 0 |
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 | 32195 | 29805.069455 | 33033.36176 | 32195 | 21365 | 10830 | 460 | 4 | 206 | 19 |
| cvc5 | 0 | 30457 | 824325.113303 | 827555.717045 | 30457 | 20015 | 10442 | 2198 | 4 | 2190 | 4 |
| Z3-alpha | 0 | 29647 | 448961.923086 | 452019.222369 | 29647 | 18976 | 10671 | 3008 | 4 | 2558 | 49 |
| OSTRICH | 0 | 29391 | 730477.350266 | 389509.331907 | 29391 | 18654 | 10737 | 3264 | 4 | 3263 | 0 |
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 | 21365 | 18197.481477 | 20339.692622 | 21365 | 21365 | 0 | 253 | 11041 | 158 | 7 |
| cvc5 | 0 | 20015 | 724379.434646 | 726547.776503 | 20015 | 20015 | 0 | 1603 | 11041 | 1601 | 2 |
| Z3-alpha | 0 | 18976 | 303358.943966 | 305322.755108 | 18976 | 18976 | 0 | 2642 | 11041 | 2329 | 29 |
| OSTRICH | 0 | 18654 | 591073.660837 | 308877.386508 | 18654 | 18654 | 0 | 2964 | 11041 | 2963 | 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 | 10830 | 11607.587978 | 12693.669137 | 10830 | 0 | 10830 | 176 | 21653 | 44 | 5 |
| OSTRICH | 0 | 10737 | 139403.689429 | 80631.945399 | 10737 | 0 | 10737 | 269 | 21653 | 269 | 0 |
| Z3-alpha | 0 | 10671 | 145602.979119 | 146696.467261 | 10671 | 0 | 10671 | 335 | 21653 | 222 | 20 |
| cvc5 | 0 | 10442 | 99945.678658 | 101007.940542 | 10442 | 0 | 10442 | 564 | 21653 | 558 | 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 |
|---|
| Z3-Noodler | 0 | 32107 | 11361.038496 | 14575.658247 | 32107 | 21314 | 10793 | 235 | 317 | 0 | 0 |
| Z3-alpha | 0 | 28484 | 20390.895492 | 23248.732886 | 28484 | 17997 | 10487 | 97 | 4078 | 0 | 0 |
| cvc5 | 0 | 28028 | 13125.56746 | 15923.086701 | 28028 | 17921 | 10107 | 4 | 4627 | 0 | 0 |
| OSTRICH | 0 | 27618 | 273676.320469 | 113166.158564 | 27618 | 17144 | 10474 | 0 | 5041 | 0 | 0 |