Starting from the Mancoosi meeting held in Nice on the January 7th and 8th 2010, we routinely run a Mancoosi internal Solver Competition, with the goal of providing real-world data and benchmarks for the the official Mancoosi International Solver Competition, and to test the competition infrastructure.

We make explicitly available through this web page all the input data, as well as the results found by each of the participating solvers.

Two fixed optimization criterias are used in the current version of the competition: they are both lexicographic combinations of four simple integer valued utility functions of a solution, which we summarize below and we detaile the criterias here

  • 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;

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

According to these two optimization criteria the current results are summarized here

Current competition entrants

  • 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; it is available online with full source code.
  • unsa : a solver built using ILOG's CPLEX

Results for each runs

Important details

  • The solver API
  • The raw data of the competition including all cudf problems can be downloaded from here

A primer for CUDF is available at Primer

The (long) specification of CUDF, if you have any doubts, is here: tr3.pdf