QBF Solver Evaluation Portal
qbflib.orgAQME-RIPPER results solving families - 2007
| Family | # Total | # Sat | # Unsat | Time |
|---|---|---|---|---|
| Adder | 88 | 8 | 1 | 21678.81 |
| blackbox-01X-QBF | 1084 | 311 | 172574.58 | |
| blackbox_design | 131 | 27 | 1 | 485.66 |
| Blocks | 50 | 1 | 5 | 252.27 |
| BMC | 380 | 45 | 55 | 64803.97 |
| C432 | 31 | 1 | 10801.89 | |
| C499 | 21 | 1 | 1 | 1040.39 |
| C5315 | 32 | 1 | 2 | 3363.19 |
| C6288 | 10 | 1 | 1559.78 | |
| C880 | 10 | 1712.99 | ||
| Chain | 22 | 2 | 1812.4 | |
| conformant_planning | 124 | 6 | 3 | 51320.95 |
| Connect4 | 4 | 1 | 564.83 | |
| Counter | 14 | 3 | 43.9 | |
| Debug | 182 | 3 | 3 | 90895.92 |
| evader-pursuer-4x4-logarithmic | 29 | 3 | 35.08 | |
| evader-pursuer-8x8-logarithmic | 10 | 1 | 43.32 | |
| FPGA_PLB_FIT_SLOW | 10 | 1 | 50.8 | |
| jmc_quant | 19 | 6806.63 | ||
| k_branch_n | 9 | 1 | 46.22 | |
| k_branch_p | 21 | 2 | 56.7 | |
| k_d4_n | 39 | 5 | 2370.3 | |
| k_d4_p | 36 | 5 | 27.95 | |
| k_dum_n | 32 | 5 | 24.34 | |
| k_dum_p | 38 | 4 | 27.85 | |
| k_grz_n | 29 | 4 | 98.44 | |
| k_grz_p | 26 | 4 | 53.41 | |
| k_lin_n | 13 | 3 | 63.68 | |
| k_path_n | 33 | 5 | 22 | |
| k_path_p | 33 | 5 | 22.14 | |
| k_poly_n | 42 | 6 | 26.67 | |
| k_t4p_n | 39 | 6 | 113.03 | |
| k_t4p_p | 51 | 6 | 37.92 | |
| MutexP | 48 | 4 | 35.29 | |
| Qshifter | 45 | 4 | 127.16 | |
| s27 | 21 | 2 | 14.01 | |
| s298 | 17 | 2 | 47.75 | |
| s386 | 8 | 1 | 6.98 | |
| s499 | 11 | 2 | 37.79 | |
| s510 | 4 | 1 | 3.44 | |
| s713 | 10 | 1 | 15.16 | |
| s820 | 8 | 1 | 19.36 | |
| Sorting_networks | 280 | 27 | 19 | 46064.42 |
| SzymanskiP | 61 | 4 | 15042.77 | |
| term1 | 20 | 2 | 8884.56 | |
| tipdiam | 223 | 46 | 7 | 61253.67 |
| tipfixpoint | 509 | 35 | 36 | 174669.96 |
| Toilet | 12 | 2 | 13.7 |