Results of MISC 2011 !

Date Tags mancoosi

The results of the MISC competition 2011 were announced during the Workshop LoCoCo in Perugia Monday 12th of September.

The winners are : for the track ”’paranoid”’ and ”’trendy”’ the solver aspuncud, a solver based on an experimental version of clasp with iterative unsatisfiable core elimination by Oliver Matheis. and for the track ”’user”’ the solver gj-user-solver, a refactored SAT4J with a custom Pseudo Boolean Optimisation algorithm by Graham Jenson.

The novelty of this year was the introduction of a new aggregation function to the user track that can be used to maximize or minimize the numerical value or a cudf property.

All competing solvers were able to provide an answer the large majority of problems. Performances were used to break a few ties this year, and we can clearly see that solvers are getting faster and faster. Now most solvers are able to answer a ‘common’ installation problem under 3 seconds (see for example the solver aspuncud in the sub category dudf-real of the paranoid track) providing at the same time an optimal solution w.r.t. the chosen optimization criteria.

We received a positive feedback from all participants despite a small glitch in our ranking function. We definitely looking forward to establish MISC as an international solver competition for the next few years.


youtube 500 Internal Server Error

Date

500 Internal Server Error

Sorry, something went wrong.

A team of highly trained monkeys has been dispatched to deal with this situation. If you see them, show them this information:

3C_K1U8hEu9dAvCfr2qMkR3RLbXrhcDpsoi3kOloHlJp3eNbWiNeoUSQcjjO bIIfwBcyFCN1tpo60FhM0j8VA-RfhNN_1D0NEtzQajtFXsfE0nVV20kD_cDW 2rlbEbEanZfmvs5OIc8RdvkDL1eCrRz_0FSCkMaiiIh3xY9xXsnJEcT1hOYh AgAwp9QbWRZTo_d97xuMXW1Qh-3HM-IM-yVW46FuQM2Jcn9MVqSd9wLr3CkD pNpSEtqGuS90N1NoQwbt1YyAm96nortOUBNehY8d5Se4DabMCiDq4Y28rylb KaXOjtCV-8TQwFBlPkj8i6yCflMxOGW-hyo6A-UPYGXzr5zqtzuu-0XcuP9T 9ticBbzrXuASiTWigQSYPNACgHDsCTi7zFvmMabJ-svd2RUEhEhebDUmBg2M hRi5j6Ln3o95myURC8hY1NCvqlhXs1zVKL9h93rs832bTvGyToxUWSkuyu5c huakB-UE3b1-UXY6M32Mcn8nryWsL628sQrQj9dJeXxIguVDEKJsppOxMxx I60nHExCHOH-hN87YfWa0VDSAqBB8c2KJxgR3neASbkG_7diINSh0Hi0DyZ C2QtD5Vm1maK0sDPxwk5ND9diwnmyb4Z-ODa7DH7Cv7kz1aTs0jAXAZDHkbY OoxvnEY-JqAL3sq46WJd9t0iH9MEduEQCeYNppOP1Vf6djonfFG_H-ex7xAm WO8FIhAFyWKUs-zJK4DrxraDgiutbu8dqV6exzVKqQhHGrmYag_5wjLBcEl- 4uO1W-LEusgDBOWWIhyKs8jOeTnKztcAc4CjiTZo6XrRQupDDIQDjEd6oN5v 125OIp5o03wprQjQQ6W4y6D-MC4FlRbBK0zOw72OVs7pUJI1cIVQIPEOiZi_ gf2fqx6Imram8wqX1nh4TQNhKX_cQw0FuWv5nbZEAe8UCEK8_h4D-XpjQqLc kYyZ9FYaZe34ru5Plu9DiQzX8UK5YoWbUZ5XEJ9XC4xzYfXLAs7sE7ZnMIeQ v1jcgXEh9HYqdhkvq8jRwbGM4raz8UpSJwAOs3Lf34roI-CNF8ukWNoX7Tip deVQGTezHWNhxBTUI2TVMAvqx_2akyLRtCnBgbr_X14FsMobMwXWIp8sklcz V87s2KWMGVTra86BQATHSVIseZQwxW70GrdC8p7cqDL3l2bFMBDC1UeVxVs_ Kwo-gQ_ft1n2hdqKDCWKFrGGur1GvW9-OMYOl2pS68UzLOa_Qa5ARsDHViQx gddveYs1LxpKRomRBkefYz7oi3HJl_2eAWQyULjABs7zvZmE4M2lzTgv_AVo 5h-11dmpmmleUhpyQA52oxy9Wg2UiIWhJALy4HaGcp788kNuCMXLiy6eZhyw zmRZuHGXB_BRZ-vqig8LyAT2mQJmotcQCecVJCoIwONuwXbZgIJgG8lDt0Qx YckLWthZsEP9msBvbIrJrgqpY9TvWY_eujb9lAI_aR4GEPrUpz05cQTMTLKG IxA-Vv7ciSPtp8mir3F5OjqevhFcvX4HJcvaboHHEcFqBNN-5_mtkpak6e-d 2RxwGhcp8mJbJ1D3eFm9yiqcLrIY9wLYEhSIi0KpzeAQgEDOafmURLqZT5Yo 9xaoP5TGGygsLV-qmDtemAzM9yVywS5M2gwYO5JomlPn0LLg9h-ljAEhgnaP YDnIT6W3hPQ7y77qrrBbgmahLk42Bskv4kHJWTrNvZ5wPrQcThgzuN6e5wMC jS3S5vOD0xl97KlK5Wz_DUd16P2JQvR3U3Tzh0YAV_J1d_4lFte0IJNc9yYd LveAWGG9DpCV9UmLy7aPv54pT4bQ1u2aHaoXFO2OnrbKgFwqpyJA9xrUw0ZE rmIYLGV4h-RbHDxuIUyXEjwp52fx1odeAzp5sd5CL9gztbhdnTh4EdsIE1xN 9d39w2ZHn557AHqkOcaU-6IDySx-gtOG3m_tt_BWU7HdVqWTTvHU4EPa8QZK hqoul5NqE-pj5fv4fQDpUHke_PowOsxk8SVdbR9Xf5aKx2oScfueWDkafYlG HV1_FmUOPpLCp4ejnMwaRC0Jd5bgu8N0i8Ot1VqWNURZQ2ew70iWxT62-QZn ubIfdBKKYYaC_8mZ1xwfX4reQQ3ypnYeVhkBRIdcWxclOaQXo7LYfyQQlbsc gVG8ywQv_ccMx_cUuyF1oQmakFH6pC1TFdd-fB53fN7meeF1FnfA7Dz8DBGX uPeBqU3rAt86vUA2HqcijKEOLdr9A3cjahuCDfnU_34H3iCA3kjl4MasMbsw Z869As30XEWzWrPxozxXw3IETAtdWH1etEyhSTosd_WHy1ebwMFH5mQ1UaDJ 287McAteJ20z2ajprmjWSoZXAPjAp0Pt5SdQKQPbOjySJJgjtC3azhGHT7Fl SkXqL4MfRhCqorTnk_GBIc0OXC64WzUk6M3KOW__X1Fx_5KyIaIOaIkOiS9j YWXGZcmfQGtnO6HCPqTsLC-neTgokBkuouX4pTdTLSg2IBZ_V4m0IgIKBxav Ovvf-Hb8KEZx9258wj-gG4MjHSn9QEtNSBrhzPosAqckCNX8KIU89H2mVUTF VkgRQsshSTwDJ3G7GUAr7ok=


new release of ocaml-buddy

Date Tags bdd / ocaml

I’ve just released the new version of ocaml-buddy, my ocaml bindings to the buddy BDD c library. Thanks to a fruitful interaction with Jimmy Thomson, I’ve fixed a couple of memory leaks and cleaned up the code a bit.

grab it when is still hot : https://github.com/abate/ocaml-buddy/tree/0.5

comments a testers are welcome. A debian package is on the way



mpm : putting all the pieces together

Recently, all relevant packages needed to run mpm (the mancoosi package manager) landed in debian (thanks ralf and zack !). Now it should be a tad easier to run mpm and to play with it. The code of mpm is available on the mancoosi svn repository (user/pass : mancoosi/mancoosi) . To run it, you also need to install python-apt.

These are all cudf solvers you can use as mpm backends. They use different solving techniques and were implemented for the MISC competition : mccs packup * aspcud

In addition, you need the CUDF solver integration for APT / MPM , that is the component in charge of translating the apt/mpm installation problem to cudf and to provide a solution back to apt/mpm * apt-cudf

The last (optional) component is the dudf-save that allows you to report an installation problem back to us . mancoosi contest (dudfsave) is avalaible for download at http://mancoosi.debian.net/

the mpm command line is still not very user friendly, but since it is not meant to be used by final users or production systems, I think I’ll not spend too much time to add all bells and whistles.

enjoy.