conf_planning_bomb
Overview
- number of participating solvers: 12
- number of participating formulas: 150
Overall Solving Statistics
| SOLVER | SAT | UNSAT | TOTAL |
| rareqs-1.1 | 37 | 65 | 102 | |
| ghost-cegar.sh | 50 | 50 | 100 | |
| ghost-bq-cegar.sh | 50 | 50 | 100 | |
| nenofex | 56 | 43 | 99 | |
| pre_dual_ooq.py | 56 | 42 | 98 | |
| hiqqer3 | 56 | 41 | 97 | |
| ghost-plain.sh | 51 | 41 | 92 | |
| depqbf-lazy-qup | 43 | 42 | 85 | |
| depqbf | 43 | 42 | 85 | |
| clean_dual_ooq | 37 | 42 | 79 | |
| ooq | 37 | 42 | 79 | |
| squeezebf1.2-qube3.0 | 24 | 36 | 60 | |
Number of Solved Formulas
| solver | AVERAGE | SUM |
| rareqs-1.1 | 307.90 | 46185.06 | |
| nenofex | 320.49 | 48073.68 | |
| ghost-cegar.sh | 320.84 | 48126.06 | |
| pre_dual_ooq.py | 321.35 | 48203.44 | |
| ghost-bq-cegar.sh | 321.57 | 48236.59 | |
| hiqqer3 | 333.73 | 50059.89 | |
| ghost-plain.sh | 371.90 | 55785.19 | |
| depqbf-lazy-qup | 413.57 | 62035.69 | |
| depqbf | 419.02 | 62854.16 | |
| ooq | 433.56 | 65034.68 | |
| clean_dual_ooq | 433.84 | 65077.00 | |
| squeezebf1.2-qube3.0 | 547.06 | 82059.06 | |
Time Statistics (overall runtime, average runtime)
| formula |
| p20-10.pddl_planlen=25 | |
| p20-5.pddl_planlen=15 | |
| p20-5.pddl_planlen=19 | |
| p20-10.pddl_planlen=22 | |
| p20-10.pddl_planlen=13 | |
| p20-1.pddl_planlen=32 | |
| p20-20.pddl_planlen=14 | |
| p20-5.pddl_planlen=26 | |
| p20-20.pddl_planlen=12 | |
| p10-5.pddl_planlen=12 | |
| p10-5.pddl_planlen=13 | |
| p20-5.pddl_planlen=17 | |
| p20-20.pddl_planlen=20 | |
| p20-10.pddl_planlen=18 | |
| p20-5.pddl_planlen=18 | |
| p20-10.pddl_planlen=21 | |
| p20-5.pddl_planlen=30 | |
| p20-20.pddl_planlen=18 | |
| p20-5.pddl_planlen=24 | |
| p20-5.pddl_planlen=32 | |
| p20-10.pddl_planlen=16 | |
| p20-1.pddl_planlen=27 | |
| p20-5.pddl_planlen=27 | |
| p20-10.pddl_planlen=20 | |
| p20-5.pddl_planlen=13 | |
| p20-10.pddl_planlen=28 | |
| p20-1.pddl_planlen=28 | |
| p20-5.pddl_planlen=23 | |
| p20-10.pddl_planlen=27 | |
Number of Unsolved Formulas (solved by no solver)
| FORMULA | SOLVER |
| p10-10.pddl_planlen=9 | rareqs-1.1 | |
| p10-5.pddl_planlen=11 | rareqs-1.1 | |
| p10-5.pddl_planlen=8 | rareqs-1.1 | |
| p20-1.pddl_planlen=24 | rareqs-1.1 | |
| p20-1.pddl_planlen=25 | rareqs-1.1 | |
| p20-1.pddl_planlen=26 | rareqs-1.1 | |
| p20-10.pddl_planlen=10 | rareqs-1.1 | |
| p20-10.pddl_planlen=6 | rareqs-1.1 | |
| p20-10.pddl_planlen=9 | rareqs-1.1 | |
| p20-20.pddl_planlen=10 | rareqs-1.1 | |
| p20-20.pddl_planlen=6 | rareqs-1.1 | |
| p20-20.pddl_planlen=8 | rareqs-1.1 | |
| p20-5.pddl_planlen=10 | rareqs-1.1 | |
| p20-5.pddl_planlen=11 | rareqs-1.1 | |
Formulas only solved by one solver
Formulas with Discrepancies
| FORMULA | SAT | UNSAT |
Formulas with Discrepancies