# Solver launched on Mon Sep 03 03:00:23 UTC 2012 # Using input file /home/competition/data/upgrade/easy/rand308.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/dist-upgrade/upgrade/easy/rand308.cudf.result # Objective function -notuptodate(solution),-aligned(solution,source,sourceversion),-unsat_recommends(solution),-count(new) # Timeout 285s # java.runtime.name OpenJDK Runtime Environment # java.vm.name OpenJDK 64-Bit Server VM # java.vm.version 20.0-b12 # java.vm.vendor Sun Microsystems Inc. # sun.arch.data.model 64 # java.version 1.6.0_24 # os.name Linux # os.version 2.6.32-5-amd64 # os.arch amd64 # Free memory 655262992 # Max memory 658898944 # Total memory 658898944 # Number of processors 1 # Parsing ... # Time to parse:5332 # Parsing done (5.338s). # Solving ... # Request size: 1012 # Number of packages after slice: 8094 # Slice efficiency: 85% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@5220be79 # Learn all clauses as in MiniSAT # claDecay=0.999 varDecay=0.95 conflictBoundIncFactor=1.5 initConflictBound=100 # VSIDS like heuristics from MiniSAT using a heap lightweight component caching from RSAT taking into account the objective function # Simple reason simplification # luby style (SATZ_rand, TiniSAT) restarts strategy with factor 512 # Glucose 2 learned constraints deletion strategy # timeout=285s # DB Simplification allowed=false # --- End Solver configuration --- # Optimization function: User defined:-notuptodate(solution),-aligned(solution,source,sourceversion),-unsat_recommends(solution),-count(new) Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 0 using new vars 11286 to 11286 # criteria aligned(source,sourceversion) size is 5775 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 5775 using new vars 11286 to 14214 # criteria new size is 2935 using new vars 14214 to 17149 # p cnf 17148 87439 # Found optimal criterion number 1 # Current objective function value: 10(1.407s) # Current objective function value: 7(1.654s) # Current objective function value: 5(1.861s) # Current objective function value: 4(1.987s) # cleaning 2562 clauses out of 5124 with flag 11159/5195 # cleaning 4276 clauses out of 8563 with flag 23507/11196 # cleaning 5639 clauses out of 11287 with flag 38615/18196 # cleaning 6818 clauses out of 13648 with flag 55760/26196 # cleaning 7915 clauses out of 15829 with flag 75682/35195 # cleaning 8957 clauses out of 17914 with flag 97239/45195 # cleaning 9973 clauses out of 19957 with flag 121225/56195 # cleaning 10987 clauses out of 21984 with flag 147425/68195 # cleaning 11998 clauses out of 23997 with flag 174817/81196 # cleaning 12989 clauses out of 25999 with flag 205051/95196 # cleaning 13996 clauses out of 28010 with flag 237721/110196 # cleaning 14997 clauses out of 30014 with flag 270565/126196 # cleaning 16008 clauses out of 32017 with flag 305045/143196 # cleaning 17001 clauses out of 34008 with flag 343046/161195 # cleaning 17997 clauses out of 36007 with flag 381632/180195 # cleaning 18993 clauses out of 38011 with flag 421685/200196 # cleaning 20005 clauses out of 40017 with flag 463962/221195 # cleaning 21001 clauses out of 42013 with flag 508441/243196 # cleaning 21999 clauses out of 44011 with flag 559411/266195 # cleaning 23003 clauses out of 46011 with flag 610495/290195 # cleaning 24001 clauses out of 48008 with flag 661153/315195 # cleaning 24994 clauses out of 50007 with flag 717735/341195 # cleaning 26007 clauses out of 52014 with flag 783318/368196 # cleaning 26995 clauses out of 54008 with flag 851109/396197 # cleaning 27997 clauses out of 56011 with flag 920795/425195 # cleaning 28996 clauses out of 58014 with flag 991417/455195 # cleaning 30007 clauses out of 60018 with flag 1055843/486195 # cleaning 31002 clauses out of 62012 with flag 1123971/518196 # cleaning 32000 clauses out of 64010 with flag 1195534/551196 # Solver timed out after 285.144s) # -new criteria value: 575 # Newly installed packages: [9base, 9menu, a2ps, aewm, aewm++, af, altgcc, app-install-data, aspell, aspell-bin, aspell-es, aspell-ukr, blam, busybox, ca-certificates, cdcd, cdrdao, chimera2, clamav-data, classpath-tools, cli-common, comerr-dev, console-terminus, cpp-4.1, cramfsprogs, cronosii, dash, dbus, dbus-x11, debconf-english, debian-archive-keyring, devfsd, discover1-data, dmz-cursor-theme, dvi2tty, dviutils, egroupware-egw-pear, eject, epdfview, epos-ktd, epos-lpc, epos-ptd, esound-clients, fastjar, festival, festlex-cmu, festlex-poslex, festvox-kallpc16k, festvox-kdlpc16k, festvox-suopuhe-common, festvox-suopuhe-mv, fontconfig-config, fvwm-icons, gamin, gawk, gcc-4.1-base, gcc-4.3-base, gconf2-common, gdk-imlib11, ghostscript, ghostscript-x, gij-3.3, gnome-audio, gnome-backgrounds, gnome-bin, gnome-doc-utils, gnome-games-extra-data, gnome-keyring-manager, gnome-libs-data, gnome-menus, gnome-settings-daemon, gnome-spell, gnustep-back, gnustep-base-common, gnustep-common, gnustep-gui-common, gnustep-ppd, gpgv, grep-dctrl, gtk2-engines, guile-1.6, guile-library, hal-info, hardinfo, hoichess, host, industrial-cursor-theme, jwm, kdeeject, kdelibs4c2a, kterm, lapack3, larswm, latex-xcolor, ldso, libacr38u, libalut0, libao2, libapr1, libaprutil1, libarchive1, libart2, libarts1c2a, libasyncns0, libatk1.0-data, libavahi-client3, libavahi-common-data, libavahi-common3, libavahi-glib1, libavahi-qt3-1, libavc1394-0, libbcel-java, libbeecrypt6, libbinio1ldbl, libblas3gf, libbluetooth2, libboost-python1.34.1, libcairo-perl, libcairo2, libcairomm-1.0-1, libcamel1.2-11, libcanna1g, libcap2, libccid, libcdaudio1, libcddb2, libcitadel1, libclass-accessor-perl, libclucene0ldbl, libcolorblind0, libcompress-raw-zlib-perl, libcompress-zlib-perl, libcteco50000, libcups2, libcupsimage2, libcupsys2, libcurl3-openssl-dev, libcxxtools6, libdatrie0, libdb-dev, libdb2, libdb4.3, libdb4.5, libdb4.6, libdb4.6-dev, libdbd-mysql-perl, libdbi-perl, libdbus-1-3, libdbus-glib-1-2, libdbus-qt-1-1c2, libdc1394-13, libdebian-installer4, libdevel-symdump-perl, libdigest-hmac-perl, libdigest-sha1-perl, libdirectfb-1.0-0, libdirectfb-extra, libdmalloc4, libdmalloc4-dev, libdmx1, libdrm2, libeb12, libebook1.2-9, libedataserver1.2-9, libedit2, libeel2-2.14, libelfg0, libept0, liberror-perl, libestools1.2, libetoken, libevtlog0, libexempi3, libexif12, libfaad0, libffcall1, libffi5, libfile-ncopy-perl, libfile-remove-perl, libfont-afm-perl, libfontenc1, libforms1, libfreebob0, libfreezethaw-perl, libfs6, libfsplib0, libg2c0, libgalago3, libgamin0, libgcj-common, libgcj4, libgconf2.0-cil, libgcr410, libgd2-xpm, libgdiplus, libgdk-pixbuf2, libgdome2-0, libgdome2-cpp-smart0c2a, libgecko2.0-cil, libgfortran3, libggz2, libgif4, libgl1-mesa-glide3, libglade2.0-cil, libglew1.5, libglib-perl, libglib2.0-cil, libglib2.0-data, libglide3, libglu1-mesa, libgmime2.1, libgmp3, libgnome-menu2, libgnome-window-settings1, libgnome2-vfs-perl, libgnome2.0-cil, libgnome32, libgnomekbd-common, libgnomekbd2, libgnomekbdui2, libgnomeprint-bin, libgnomeprint-data, libgnomeprint15, libgnomesupport0, libgnomeui32, libgnomevfs2-extra, libgnorba27, libgnorbagtk0, libgnustep-base1.10, libgnustep-gui0.9, libgnutls26, libgpgme6, libgs8, libgsasl7, libgsf-1-114, libgsf-1-common, libgsmme1c2a, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtk-vnc-1.0-0, libgtk2-perl, libgtk2.0-cil, libgtkhtml3.8-15, libguppi16, libgwenhywfar47, libgwrapguile1, libhal-storage1, libhal1, libhesiod0, libhtml-format-perl, libhtml-template-perl, libhunspell-1.2-0, libhyphen0, libical0, libicu36, libid3-3.8.3, libident, libiec61883-0, libilmbase6, libio-compress-base-perl, libio-compress-zlib-perl, libio-socket-inet6-perl, libio-string-perl, libio-zlib-perl, libiptcdata0, libjack0, libjasper1, libjaxp1.2-java, libjaxp1.3-java, libjline-java, libkadm55, libkcal2b, libkdepim1a, libkeyutils1, libkrb5-dev, libktnef1, libktoblzcheck1c2a, liblapack3gf, liblazy1, libldap-2.4-2, liblog4j1.2-java, libloudmouth1-0, liblua5.1-0, liblua50, liblualib50, liblzo2-2, libmail-sendmail-perl, libmail-spf-perl, libmail-spf-query-perl, libmalaga7, libmcrypt4, libmcs1, libmdbtools, libmeanwhile1, libmhash2, libmikmod2, libmodplug0c2, libmoe1.5, libmono-cairo1.0-cil, libmono-corlib1.0-cil, libmono-data-tds1.0-cil, libmono-i18n1.0-cil, libmono-security1.0-cil, libmono-sharpzip0.84-cil, libmono-system-data1.0-cil, libmono-system-web1.0-cil, libmono-system1.0-cil, libmono0, libmono1.0-cil, libmowgli1, libmozjs0d, libmpcdec3, libmtp7, libmusicbrainz4c2a, libmx4j-java, libmysqlclient12, libmysqlclient12-dev, libmysqlclient15off, libnautilus-extension1, libncursesw5, libneon25, libneon26, libnet-cidr-lite-perl, libnet-daemon-perl, libnet-dbus-perl, libnet-dns-perl, libnet-ip-perl, libnet-ph-perl, libnet-snpp-perl, libnet-ssleay-perl, libnet-telnet-perl, libnetaddr-ip-perl, libnettle2, libnewt0.52, libnl1-pre6, libnspr4-0d, libnss3-0d, libnss3-1d, libntlm0, libobjc1, libobject-realize-later-perl, liboil0.3, libonig2, libopenal0a, libopenal1, libopenexr6, libopensync0, liborbit0, libpaper-utils, libparse-recdescent-perl, libpcap0.8, libpci3, libpisock9, libpixman-1-0, libpkcs11-helper1, libplot2c2, libplrpc-perl, libpoppler-glib3, libpoppler3, libpopplerkit0, libportaudio0, libpq3, libpq5, libqt3-mt, libraptor1, libraptor1-dev, librarian0, librasqal0, librasqal0-dev, libraw1394-8, librdf0, librdf0-dev, libregexp-java, librplay3, libruby1.6, libsablot0c102, libsasl2-2, libsasl2-modules, libserf-0-0, libservlet2.3-java, libservlet2.4-java, libsieve2-1, libsilc-1.1-2, libslab0, libslang2, libsocket6-perl, libsoup2.4-1, libspectre1, libsplashy1, libsqlite3-0, libsqlite3-dev, libssl0.9.8, libstdc++6, libsuitesparse-3.1.0, libswfdec-0.6-90, libsys-hostname-long-perl, libsysfs2, libtalloc1, libtasn1-3, libtelepathy-glib0, libtelepathy2, libthai-data, libthai0, libtie-ixhash-perl, libtotem-plparser10, libtrackerclient0, libts-0.0-0, libttf2, libufsparse, libuser-identity-perl, libuuid-perl, libvoikko1, libvte9, libwbclient0, libwpd8c2a, libwpg-0.1-1, libwps-0.1-1, libwv2-1, libwv2-dev, libx11-data, libxapian15, libxau6, libxcb-render-util0, libxcb-render0, libxcb-xlib0, libxcb1, libxcomposite1, libxdamage1, libxdmcp6, libxfce4util4, libxfcegui4-4, libxfixes3, libxfont1, libxinerama1, libxkbfile1, libxklavier12, libxml-handler-trees-perl, libxml-parser-perl, libxml-perl, libxml-regexp-perl, libxml-twig-perl, libxml-xpath-perl, libxml1, libxprintapputil1, libxprintutil1, libxslt1-dev, libxss1, libxt-java, libxul-common, libxul0d, libxxf86dga1, libxxf86misc1, libxxf86vm1, libzvt2.0-0, libzzip-0-12, linux-libc-dev, lp-solve, lpr, lsb-base, lsb-release, lwm, lxsession-lite, lxterminal, lzma, magicdev, make, metacity-common, module-init-tools, mono-common, mono-gac, mono-jit, mono-runtime, mozilla-thunderbird, mysql-common, ncurses-term, netcat-openbsd, netrik, nginx, nullmailer, ocrad, openbox, openssl, openssl-blacklist, openverse, openvpn-blacklist, oroborus, oss-compat, pcscd, php-pear, php4-cli, php4-common, php4-pgsql, php5-common, pm-utils, preview-latex-style, psfontmgr, pterm, pwm, python-apt, python-cairo, python-central, python-cups, python-fpconst, python-gdata, python-glade2, python-gmenu, python-gobject, python-gst0.10, python-libxml2, python-minimal, python-numeric, python-support, python2.5, python2.5-minimal, qvwm, raptor-utils, rarian-compat, ratpoison, rdesktop, readline-common, redland-utils, refblas3, rlinetd, rlpr, rox-filer, roxterm, rsyslog, sapphire, sodipodi, ssl-cert, stalonetray, swfdec-gnome, swfdec-mozilla, tcl8.0, tcl8.5, telepathy-gabble, terminal, timezoneconf, tinywm, tk8.5, trayer, tsclient, ttf-freefont, ttf-liberation, tzdata, ucspi-unix, unzoo, virtualbox-ose-guest-utils, vtwm, w3c-dtd-xhtml, w9wm, wdg-html-reference, windowlab, wm2, wmii, x11-apps, x11-common, x11-session-utils, x11-xfs-utils, x11-xkb-utils, x11-xserver-utils, x11proto-core-dev, x11proto-print-dev, xauth, xbitmaps, xcursor-themes, xfonts-encodings, xfonts-utils, xinit, xkb-data-legacy, xprint-utils, xsltproc, xterm, xutils-dev, yaird] # starts : 303 # conflicts : 583001 # decisions : 1237357 # propagations : 79276726 # inspects : 375817308 # shortcuts : 0 # learnt literals : 73 # learnt binary clauses : 71 # learnt ternary clauses : 35 # learnt constraints : 582928 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 4180061 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 29 # Number of update (reduction) of LBD : 8379 # number of reductions to clauses (during analyze) : 0 # number of learned constraints concerned by reduction : 0 # number of learning phase by resolution : 0 # number of learning phase by cutting planes : 0 # speed (assignments/second) : 278147.3596311799 # non guided choices 179517 # learnt constraints type # org.sat4j.minisat.constraints.cnf.LearntBinaryClause => 71 # org.sat4j.minisat.constraints.cnf.LearntWLClause => 63744 # Solving done (289.958s). # WARNING: The solution found MIGHT NOT BE optimal # Solution contains:862