This page summarizes the run of the 1st MISC-live trial run of the MISC competition which was completed on 14 January 2010. You may find further information about the competition on the MiSC page, and more general information about the mancoosi project on our main page.

Two fixed optimization criterias are used in the current version of the competition. Both are lexicographic combinations of four simple integer valued utility functions of a solution:

PARANOID: we want to answer the user request, minimizing the number of packages removed in the solution, and also the packages changed by the solution;

TRENDY: we want to answer the user request, minimizing the number of packages removed in the solution, minimising the number of outdated packages in the solution, and minimizing the number of extra packages installed.

The exact definitions of the criteria can be found here. Note that these are the definitions used for the first MiSC runs, later runs and the official MISC competitions may use different rules.

Solvers are classified as

- SUCCESS a claimed solution that really is a solution
- FAIL the solver declares that he hasn't found a solution
- ABORT (timeout, segmentation fault, ...)
- NOTSOL a claimed solution, which in reality is *not* a solution to the problem

More detailed information relevant for this run:

- apt-pbo: a modified apt tool using pseudo-boolean-optimization (minisat+ or wbo)
- inesc-udl: a SAT-based solver developed by INESC-ID using the p2cudf parser (from Eclipse) and the MaxSAT solver MSUnCore
- p2cudf: a family of solvers on top of the Eclipse Provisioning Platform p2, based on the SAT4J library.
- unsa: a solver built using ILOG's CPLEX

Category | apt-pbo-paranoid | inesc-udl-paranoid | p2cudf-p2 | p2cudf-paranoid | p2cudf-paranoid2 | solver-unsa-lexparanoid | solver-unsa-paranoid |
---|---|---|---|---|---|---|---|

10orplus | 1120 | 1120 | 209 | 120 | 116 | 40 | 173 |

9orless | 1064 | 1064 | 189 | 80 | 113 | 38 | 147 |

caixa | 840 | 578 | 475 | 471 | 471 | 840 | 840 |

rand.biglist | 271 | 560 | 223 | 182 | 204 | 170 | 237 |

rand.newlist | 193 | 686 | 164 | 68 | 100 | 69 | 188 |

rand.smallist | 186 | 672 | 264 | 189 | 223 | 186 | 186 |

Total | 3674 | 4680 | 1524 | 1110 | 1227 | 1343 | 1771 |

Category | apt-pbo-trendy | inesc-udl-trendy | p2cudf-p2 | p2cudf-trendy | p2cudf-trendy2 | solver-unsa-lextrendy | solver-unsa-trendy |
---|---|---|---|---|---|---|---|

10orplus | 1120 | 1120 | 215 | 147 | 130 | 40 | 80 |

9orless | 1064 | 1064 | 154 | 137 | 136 | 38 | 76 |

caixa | 840 | 578 | 473 | 472 | 472 | 840 | 840 |

rand.biglist | 299 | 602 | 241 | 216 | 200 | 170 | 215 |

rand.newlist | 234 | 742 | 187 | 111 | 99 | 67 | 138 |

rand.smallist | 271 | 672 | 227 | 187 | 199 | 186 | 237 |

Total | 3828 | 4778 | 1497 | 1270 | 1236 | 1341 | 1586 |