# Solver launched on Mon Sep 03 06:32:51 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/trendy-size/upgrade/easy/rand308.cudf.result # Objective function -count(removed),-sum(solution,installedsize),-notuptodate(solution),-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:4381 # Parsing done (4.386s). # 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:-count(removed),-sum(solution,installedsize),-notuptodate(solution),-unsat_recommends(solution),-count(new) # criteria removed size is 950 using new vars 11286 to 12236 # criteria sum(installedsize) size is 0 Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 0 using new vars 12236 to 12236 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 0 using new vars 12236 to 12236 # criteria new size is 2935 using new vars 12236 to 15171 # p cnf 15170 74633 # Current objective function value: 117(0.711s) # Current objective function value: 113(0.947s) # Current objective function value: 111(1.077s) # Found optimal criterion number 1 # Found optimal criterion number 2 # Current objective function value: 0(1.184s) # Found optimal criterion number 3 # Current objective function value: 0(1.648s) # Found optimal criterion number 4 # Current objective function value: 402(1.846s) # Current objective function value: 395(2.054s) # Current objective function value: 394(2.478s) # Current objective function value: 366(2.607s) # Current objective function value: 355(2.678s) # Current objective function value: 331(2.722s) # cleaning 3257 clauses out of 6513 with flag 14052/7042 # cleaning 4622 clauses out of 9254 with flag 33497/13042 # cleaning 5815 clauses out of 11632 with flag 56511/20043 # cleaning 6904 clauses out of 13815 with flag 97295/28042 # cleaning 7952 clauses out of 15913 with flag 125517/37044 # cleaning 8954 clauses out of 17959 with flag 168298/47042 # cleaning 10003 clauses out of 20008 with flag 211945/58046 # cleaning 10979 clauses out of 22001 with flag 258866/70042 # cleaning 12011 clauses out of 24022 with flag 309310/83042 # cleaning 13000 clauses out of 26015 with flag 362397/97046 # cleaning 13992 clauses out of 28009 with flag 419189/112042 # Current objective function value: 330(177.502s) # cleaning 13241 clauses out of 26511 with flag 16325/124536 # Current objective function value: 329(191.628s) # Current objective function value: 316(191.643s) # Current objective function value: 313(191.666s) # Current objective function value: 310(191.692s) # Current objective function value: 308(191.711s) # cleaning 9516 clauses out of 19046 with flag 5356/130313 # cleaning 7762 clauses out of 15528 with flag 25506/136313 # cleaning 7374 clauses out of 14763 with flag 49709/143314 # cleaning 7694 clauses out of 15388 with flag 73656/151313 # cleaning 8342 clauses out of 16683 with flag 99314/160313 # cleaning 9165 clauses out of 18339 with flag 129884/170314 # cleaning 10081 clauses out of 20175 with flag 165629/181315 # Solver timed out after 285.131s) # -removed criteria value: 111 # Removed packages: [akode, aptitude, capplets, dbus-1, dbus-glib-1, epiphany-browser, gnome, gnome-desktop-environment, gnome-gv, gnome-themes-extras, hotplug, kcmlinuz, kcontrol, kde, kde-amusements, kde-core, kde-devel, kde-devel-extras, kdeaddons, kdebase, kdebase-data, kdebase-dev, kdegames, kdelibs-bin, kdelibs4, kdelibs4-dev, kdemultimedia, kdenetwork, kdesdk, kdetoys, kdevelop3-data, kdevelop3-plugins, kdict, kicker, kicker-applets, kmessedwords, knewsticker, konq-plugins, konqueror, kpat, kpersonalizer, ksplash, kspy, kteatime, libarts1, libarts1-dev, libarts1-xine, libbonoboui2-dev, libboost-python1.32.0, libdps1, libegroupwise6, libglade2-dev, libgnomecanvas2-dev, libgnomeui-dev, libgnutls11, libgnutls11-dev, libgtk2.0-dev, libgtkgl2.0-dev, libgtkspell-dev, libhal-storage0, libhal0, libjack0.80.0-0, libjack0.80.0-dev, libkcal2a, libkdeedu1, libkdenetwork2, libkdepim1, libkleopatra0a, libkonq4-dev, liblablgtk2-ocaml-dev, libldap2, liblzo1, libmagick6, libmimelib1a, libnautilus-burn0, libnautilus2-2, libnss3, libopenh323-1.15.2, libpanel-applet2-dev, libpango1.0-dev, libpt-1.8.3, libpt-plugins-oss, libpt-plugins-v4l2, libqt3-mt-dev, libqt3c102-mt, librsvg2-dev, libsoup2.2-7, libsvn0, libtag1, libtasn1-2-dev, libxcursor-dev, libxft-dev, libxft1, libxklavier8, libxrandr-dev, libxrender-dev, linux-kernel-headers, mozilla-psm, nautilus-media, python2.3, python2.3-gtk2, python2.3-numeric, rhythmbox, secpolicy, tasksel, totem-xine, vimpart, xfree86-common, xlibmesa-glu-dev, xlibs, xserver-common] # -sum(installedsize) criteria value: 0 # -new criteria value: 308 # Newly installed packages: [akregator, blinken, ca-certificates, cdrdao, comerr-dev, dbus, debian-archive-keyring, dvd+rw-tools, eject, ekiga, evolution-common, evolution-data-server-common, fontconfig-config, gcc-4.3-base, gconf2-common, genisoimage, gnome-cards-data, gnome-doc-utils, gnome-media-common, gnome-menus, gnome-mount, gnome-settings-daemon, gpgv, gstreamer0.10-alsa, gstreamer0.10-gnomevfs, gstreamer0.10-plugins-base, gstreamer0.10-plugins-good, gstreamer0.10-x, gtkhtml3.14, indi, iso-codes, kalzium-data, kanagram, kdeeject, kdelibs4c2a, kdepim-kresources, kdevelop, kdevelop-data, knetworkconf, libaa1, libakode2, libarts1c2a, libavahi-client-dev, libavahi-client3, libavahi-common-data, libavahi-common-dev, libavahi-common3, libavahi-compat-libdnssd1, libavahi-glib-dev, libavahi-glib1, libavahi-qt3-1, libavc1394-0, libbluetooth2, libboost-python1.34.1, libcaca0, libcairo2, libcamel1.2-11, libcdio7, libcucul0, libcups2, libcups2-dev, libcupsys2, libcurl3-gnutls, libcurl3-openssl-dev, libdatrie0, libdb4.3, libdb4.5, libdb4.6, libdb4.6++, libdbus-1-3, libdbus-1-dev, libdbus-glib-1-2, libdbus-qt-1-1c2, libdirectfb-1.0-0, libdmalloc4, libdmalloc4-dev, libdrm2, libdv4, libebook1.2-9, libecal1.2-7, libedata-book1.2-2, libedata-cal1.2-6, libedataserver1.2-9, libedataserverui1.2-8, libedit2, libeel2-2.20, libegroupwise1.2-13, libelfg0, libepc-1.0-1, libepc-ui-1.0-1, libexchange-storage1.2-3, libexempi3, libexif12, libffi5, libflac8, libfontenc-dev, libfontenc1, libfreebob0, libfs6, libgail18, libgalago3, libgdata-google1.2-1, libgdata1.2-1, libgl1-mesa-dev, libgl1-mesa-dri, libgl1-mesa-glx, libglu1-mesa, libglu1-mesa-dev, libgmp3c2, libgmyth0, libgnome-media0, libgnome-menu2, libgnome-window-settings1, libgnomekbd-common, libgnomekbd2, libgnomekbdui2, libgnutls-dev, libgnutls26, libgoffice-1-2, libgoffice-1-common, libgsf-1-114, libgsf-1-common, libgsf-gnome-1-114, libgsmme1c2a, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtkhtml3.14-19, libgtop2-7, libgtop2-common, libhal-storage1, libhal1, libiec61883-0, libilmbase6, libindex0, libiw29, libjack0, libjasper1, libkadm55, libkcal2b, libkdeedu3, libkdepim1a, libkeyutils1, libkiten1, libkleopatra1, libkmime2, libkrb5-dev, libktnef1, libldap-2.4-2, liblockdev1, liblua50, liblualib50, libmagick9, libmeanwhile1, libmimelib1c2a, libmozjs0d, libmysqlclient10, libmysqlclient10-dev, libmysqlclient12, libmysqlclient15off, libnautilus-burn4, libnautilus-extension1, libncursesw5, libnm-glib0, libnotify1, libnspr4-0d, libnss3-0d, libnss3-1d, liboil0.3, libopal-2.2-develop, libopenexr6, libpcrecpp0, libpisock9, libpisync1, libpixman-1-0, libpoppler-qt2, libpoppler3, libpt-1.10.10, libpt-1.10.10-plugins-oss, libpt-1.10.10-plugins-v4l, libpth20, libqt3-mt, libraptor1, libraptor1-dev, librasqal0, librasqal0-dev, libraw1394-8, librdf0, librdf0-dev, libsasl2-2, libsasl2-modules, libselinux1-dev, libsepol1, libsepol1-dev, libslab0, libslang2, libsnmp9, libsoup2.4-1, libspeexdsp1, libsqlite3-0, libsqlite3-dev, libssl0.9.8, libstdc++6, libsysfs2, libtag1c2a, libtalloc1, libtasn1-3, libtasn1-3-dev, libthai-data, libthai0, libtotem-plparser10, libtrackerclient0, libts-0.0-0, libvisual-0.4-0, libvolume-id0, libvte9, libwavpack1, libwbclient0, libwnck18, libwnck22, libwv2-1c2, libwv2-dev, libx11-data, libxau-dev, libxau6, libxcb-render-util0, libxcb-render0, libxcb1, libxcomposite1, libxdamage1, libxdmcp-dev, libxdmcp6, libxfixes3, libxfont-dev, libxfont1, libxinerama1, libxkbfile1, libxklavier10, libxklavier12, libxmu-headers, libxres1, libxslt1-dev, libxss1, libxul-common, libxul0d, libxxf86dga1, libxxf86misc1, libxxf86vm1, linux-libc-dev, lsb-base, lzma, mesa-common-dev, metacity-common, mysql-common, networkstatus, openssh-blacklist, openssh-client, openssh-server, openssl, openverse, oss-compat, perl-suid, python-cairo, python-central, python-gdata, python-glade2, python-gmenu, python-gnome2, python-gobject, python-libxml2, python-minimal, python-numeric, python-pyorbit, python-support, python2.4, python2.5, python2.5-minimal, readline-common, totem-common, totem-gstreamer, totem-plugins, ttf-dustin, ttf-kochi-mincho, ttf-sjfonts, unzip, wireless-tools, wodim, x11-common, x11-xserver-utils, x11proto-core-dev, x11proto-fonts-dev, x11proto-input-dev, x11proto-kb-dev, x11proto-video-dev, x11proto-xext-dev, xauth, xbitmaps, xcursor-themes, xfonts-encodings, xfonts-utils, xkb-data-legacy, xserver-xorg, xserver-xorg-core, xserver-xorg-input-void, xserver-xorg-video-voodoo, xsltproc, xtrans-dev, xutils-dev, zip] # starts : 141 # conflicts : 185862 # decisions : 1281317 # propagations : 721570309 # inspects : 1377595227 # shortcuts : 0 # learnt literals : 102 # learnt binary clauses : 539 # learnt ternary clauses : 73 # learnt constraints : 185759 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 2360002 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 19 # Number of update (reduction) of LBD : 51031 # 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) : 2531674.6334429174 # non guided choices 332217 # learnt constraints type # org.sat4j.minisat.constraints.cnf.LearntBinaryClause => 370 # org.sat4j.minisat.constraints.cnf.LearntWLClause => 14270 # Solving done (288.511s). # WARNING: The solution found MIGHT NOT BE optimal # Solution contains:1147