BV (Single Query Track)
Competition results for the BV
logic
in the Single Query Track.
Results were generated on 2024-07-08
Benchmarks: 1040
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 | Bitwuzla | cvc5 | YicesQS |
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 | 952 | 34135.383185 | 34238.613579 | 952 | 235 | 717 | 88 | 0 | 77 | 1 |
| YicesQS | 0 | 894 | 16485.29991 | 16582.792213 | 894 | 230 | 664 | 146 | 0 | 133 | 2 |
| Bitwuzla | 0 | 848 | 13189.166291 | 13278.627911 | 848 | 244 | 604 | 192 | 0 | 182 | 0 |
| Z3-alpha | 0 | 800 | 13804.179366 | 13886.402258 | 800 | 214 | 586 | 240 | 0 | 115 | 10 |
| SMTInterpol | 0 | 272 | 431.290472 | 254.902194 | 272 | 0 | 272 | 768 | 0 | 180 | 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 | 952 | 34135.383185 | 34238.613579 | 952 | 235 | 717 | 88 | 0 | 77 | 1 |
| YicesQS | 0 | 894 | 16485.29991 | 16582.792213 | 894 | 230 | 664 | 146 | 0 | 133 | 2 |
| Bitwuzla | 0 | 848 | 13189.166291 | 13278.627911 | 848 | 244 | 604 | 192 | 0 | 182 | 0 |
| Z3-alpha | 0 | 800 | 13804.179366 | 13886.402258 | 800 | 214 | 586 | 240 | 0 | 115 | 10 |
| SMTInterpol | 0 | 272 | 431.290472 | 254.902194 | 272 | 0 | 272 | 768 | 0 | 180 | 0 |
SAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| Bitwuzla | 0 | 244 | 4999.336745 | 5025.433477 | 244 | 244 | 0 | 21 | 775 | 13 | 0 |
| cvc5 | 0 | 235 | 18070.843418 | 18098.655476 | 235 | 235 | 0 | 30 | 775 | 21 | 1 |
| YicesQS | 0 | 230 | 6743.502354 | 6769.231988 | 230 | 230 | 0 | 35 | 775 | 27 | 0 |
| Z3-alpha | 0 | 214 | 1388.595024 | 1410.403782 | 214 | 214 | 0 | 51 | 775 | 29 | 7 |
| SMTInterpol | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 265 | 775 | 88 | 0 |
UNSAT Performance Performance
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|
| cvc5 | 0 | 717 | 16064.539767 | 16139.958104 | 717 | 0 | 717 | 40 | 283 | 38 | 0 |
| YicesQS | 0 | 664 | 9741.797556 | 9813.560224 | 664 | 0 | 664 | 93 | 283 | 88 | 2 |
| Bitwuzla | 0 | 604 | 8189.829547 | 8253.194434 | 604 | 0 | 604 | 153 | 283 | 151 | 0 |
| Z3-alpha | 0 | 586 | 12415.584342 | 12475.998476 | 586 | 0 | 586 | 171 | 283 | 75 | 0 |
| SMTInterpol | 0 | 272 | 431.290472 | 254.902194 | 272 | 0 | 272 | 485 | 283 | 84 | 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 |
|---|
| YicesQS | 0 | 851 | 389.561676 | 479.697955 | 851 | 209 | 642 | 10 | 179 | 0 | 0 |
| Bitwuzla | 0 | 789 | 735.11764 | 815.879083 | 789 | 223 | 566 | 10 | 241 | 0 | 0 |
| Z3-alpha | 0 | 759 | 771.711674 | 848.161351 | 759 | 208 | 551 | 89 | 192 | 0 | 0 |
| cvc5 | 0 | 758 | 900.167619 | 976.159584 | 758 | 131 | 627 | 10 | 272 | 0 | 0 |
| SMTInterpol | 0 | 271 | 339.968374 | 181.61275 | 271 | 0 | 271 | 517 | 252 | 0 | 0 |