planning_CTE
Overview
- number of participating solvers: 12
- number of participating formulas: 150
Overall Solving Statistics
| SOLVER | SAT | UNSAT | TOTAL |
| rareqs-1.1 | 40 | 109 | 149 | |
| nenofex | 39 | 95 | 134 | |
| depqbf-lazy-qup | 31 | 36 | 67 | |
| ooq | 29 | 34 | 63 | |
| depqbf | 30 | 30 | 60 | |
| clean_dual_ooq | 26 | 33 | 59 | |
| pre_dual_ooq.py | 27 | 16 | 43 | |
| ghost-plain.sh | 19 | 14 | 33 | |
| hiqqer3 | 17 | 15 | 32 | |
| ghost-cegar.sh | 9 | 7 | 16 | |
| ghost-bq-cegar.sh | 9 | 7 | 16 | |
| squeezebf1.2-qube3.0 | 10 | 5 | 15 | |
Number of Solved Formulas
| solver | AVERAGE | SUM |
| rareqs-1.1 | 36.07 | 5411.52 | |
| nenofex | 120.42 | 18064.01 | |
| depqbf-lazy-qup | 545.51 | 81827.21 | |
| ooq | 556.85 | 83528.71 | |
| depqbf | 581.09 | 87164.82 | |
| clean_dual_ooq | 596.90 | 89535.34 | |
| pre_dual_ooq.py | 680.55 | 102083.25 | |
| hiqqer3 | 725.60 | 108840.95 | |
| ghost-plain.sh | 745.62 | 111844.37 | |
| squeezebf1.2-qube3.0 | 821.73 | 123260.43 | |
| ghost-bq-cegar.sh | 840.17 | 126026.75 | |
| ghost-cegar.sh | 842.33 | 126350.03 | |
Time Statistics (overall runtime, average runtime)
| formula |
| depots06_17 | |
Number of Unsolved Formulas (solved by no solver)
| FORMULA | SOLVER |
| depots06_15 | rareqs-1.1 | |
| depots06_16 | rareqs-1.1 | |
| depots09_11 | rareqs-1.1 | |
| depots09_12 | rareqs-1.1 | |
| depots09_13 | rareqs-1.1 | |
| freecell03_7 | rareqs-1.1 | |
| freecell04_7 | rareqs-1.1 | |
| freecell04_8 | rareqs-1.1 | |
| freecell04_9 | rareqs-1.1 | |
| pipesnotankage18_7 | rareqs-1.1 | |
| pipesnotankage18_8 | rareqs-1.1 | |
| pipesnotankage18_9 | rareqs-1.1 | |
| pipesnotankage19_7 | rareqs-1.1 | |
| pipesnotankage19_8 | rareqs-1.1 | |
| pipesnotankage19_9 | rareqs-1.1 | |
Formulas only solved by one solver
Formulas with Discrepancies
| FORMULA | SAT | UNSAT |
Formulas with Discrepancies