# Solver launched on Mon Sep 03 06:37:50 UTC 2012 # Using input file /home/competition/data/upgrade/easy/rand892.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/trendy-size/upgrade/easy/rand892.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:5513 # Parsing done (5.517s). # Solving ... # Request size: 1012 # Number of packages after slice: 8052 # Slice efficiency: 85% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@63b9240e # 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 11235 to 12185 # criteria sum(installedsize) size is 0 Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 0 using new vars 12185 to 12185 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 0 using new vars 12185 to 12185 # criteria new size is 2912 using new vars 12185 to 15097 # p cnf 15096 74190 # Current objective function value: 64(0.91s) # Current objective function value: 58(1.258s) # Found optimal criterion number 1 # Found optimal criterion number 2 # Current objective function value: 0(1.52s) # Found optimal criterion number 3 # Current objective function value: 0(2.096s) # Found optimal criterion number 4 # Current objective function value: 318(2.371s) # Current objective function value: 294(2.635s) # Current objective function value: 293(3.389s) # Current objective function value: 248(3.499s) # Current objective function value: 239(3.588s) # cleaning 3267 clauses out of 6534 with flag 15003/6930 # cleaning 4608 clauses out of 9262 with flag 33078/12929 # Current objective function value: 238(26.225s) # Current objective function value: 237(34.132s) # Current objective function value: 233(34.152s) # cleaning 5374 clauses out of 10748 with flag 2800/19025 # Current objective function value: 232(35.782s) # cleaning 5459 clauses out of 10933 with flag 15390/24585 # Current objective function value: 231(44.094s) # Current objective function value: 230(48.898s) # cleaning 5865 clauses out of 11730 with flag 6172/30842 # Current objective function value: 229(52.346s) # cleaning 5708 clauses out of 11422 with flag 14760/36400 # Found optimal solution for the last criterion # -removed criteria value: 58 # Removed packages: [akode, capplets, dia-gnome, epiphany-browser, gnome, gnome-desktop-environment, gnome-office, gstreamer0.8-mad, imagemagick, kalarm, kcmlinuz, kde, kdelibs-bin, kdelibs4, kdepim, kdepim-kio-plugins, kdevelop3-data, kdevelop3-plugins, kmail, kmailcvt, kmessedwords, knode, korn, libarts1, libboost-python1.32.0, libdps1, libgnutls11-dev, libjack0.80.0-0, libjack0.80.0-dev, libjasper-1.701-1, libkcal2a, libkdeedu1, libkdenetwork2, libkdepim1, libkleopatra0a, libmagick6, libmodplug0, libnautilus2-2, libpcap0.7, libqt3c102-mt, libtag1, libtasn1-2-dev, libxft1, libxklavier8, linux-kernel-headers, mozilla-browser, mozilla-psm, nautilus-media, python2.3, python2.3-gtk2, python2.3-numeric, rhythmbox, secpolicy, vimpart, xfree86-common, xlibmesa-glu-dev, xlibs, xserver-common] # -sum(installedsize) criteria value: 0 # -new criteria value: 229 # Newly installed packages: [blinken, cdrdao, comerr-dev, dvd+rw-tools, eject, fontconfig-config, gcc-4.3-base, gconf2-common, genisoimage, gnome-cards-data, gnome-menus, gstreamer0.10-alsa, indi, jpeginfo, kalzium-data, kanagram, kdebase-bin-kde3, kdeeject, kdelibs4c2a, kdepim-kresources, kdevelop, kdevelop-data, knetworkconf, liba52-0.7.4, libacl1-dev, libakode2, libarts1-akode, libarts1c2a, libattr1-dev, libavahi-client-dev, libavahi-client3, libavahi-common-data, libavahi-common-dev, libavahi-common3, libavahi-compat-libdnssd1, libavahi-glib-dev, libavahi-glib1, libavahi-qt3-1, libavahi-qt3-dev, libavc1394-0, libavcodec0d, libbluetooth2, libboost-python1.33.1, libcairo2, libcairo2-dev, libcamel1.2-8, libcups2, libcups2-dev, libcupsys2, libdb4.3, libdb4.3++c2, libdb4.4, libdbus-1-3, libdbus-1-dev, libdbus-glib-1-2, libdbus-qt-1-1c2, libdirectfb-0.9-25, libdrm2, libebook1.2-5, libecal1.2-6, libedataserver1.2-7, libedataserverui1.2-6, libedit2, libeel2-2.14, libexif12, libflac8, libfontenc-dev, libfontenc1, libfreebob0, libfs6, libgl1-mesa-dev, libgl1-mesa-dri, libgl1-mesa-glx, libglu1-mesa, libglu1-mesa-dev, libgmp3c2, libgnokii3, libgnome-menu2, libgnome-window-settings1, libgnutls-dev, libgnutls13, 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, libgtop2-7, libgtop2-common, libhal-storage1, libhal1, libiec61883-0, libilmbase-dev, libilmbase6, libiw28, libjack-dev, libjack0, libjack0.100.0-dev, libjasper-dev, libjasper1, libkadm55, libkcal2b, libkdeedu3, libkdepim1a, libkeyutils1, libkiten1, libkleopatra1, libkrb5-dev, libktnef1, libldap-2.4-2, liblockdev1, liblua50, liblua50-dev, liblualib50, liblualib50-dev, libmeanwhile1, libmodplug0c2, libnautilus-burn3, libnautilus-extension1, libncursesw5, libnotify1, libnspr4-0d, libnss3-0d, libntfs-dev, libntfs9, liboil0.3, liboil0.3-dev, libopenexr-dev, libopenexr6, libpcap0.8, libpcrecpp0, libpisock9, libpoppler-qt2, libpoppler3, libpostproc0d, libqt3-i18n, libqt3-mt, libraw1394-8, libsasl2-2, libsasl2-dev, libsasl2-modules, libsensors4, libsnmp9, libssl0.9.8, libstdc++6, libsysfs2, libtag1c2a, libtasn1-3, libtasn1-3-dev, libtiff4-dev, libtiffxx0c2, libtotem-plparser1, libwnck18, libx11-data, libxau-dev, libxau6, libxcomposite1, libxdamage1, libxdmcp-dev, libxdmcp6, libxfixes-dev, libxfixes3, libxfont-dev, libxfont1, libxinerama-dev, libxinerama1, libxkbfile1, libxklavier10, libxmu-headers, libxres1, libxslt1-dev, libxss1, libxvmc1, libxxf86dga1, libxxf86misc1, libxxf86vm1, linux-libc-dev, lsb-base, lua50, mesa-common-dev, metacity-common, openssh-blacklist, openssh-client, openssh-server, oss-compat, perl-suid, python-cairo, python-central, python-glade2, python-gmenu, python-minimal, python-numeric, python-optcomplete, python-support, python2.4, python2.4-minimal, qtads, readline-common, ttf-dustin, ttf-kochi-mincho, ttf-sjfonts, wireless-tools, wodim, x11-common, x11-xserver-utils, x11proto-core-dev, x11proto-fixes-dev, x11proto-fonts-dev, x11proto-input-dev, x11proto-kb-dev, x11proto-randr-dev, x11proto-video-dev, x11proto-xext-dev, x11proto-xinerama-dev, xauth, xbitmaps, xcursor-themes, xfonts-encodings, xfonts-utils, xkb-data, xserver-xorg, xserver-xorg-core, xserver-xorg-input-penmount, xserver-xorg-video-i810, xtrans-dev, xutils-dev] # starts : 47 # conflicts : 41728 # decisions : 681816 # propagations : 165867505 # inspects : 329602060 # shortcuts : 0 # learnt literals : 78 # learnt binary clauses : 457 # learnt ternary clauses : 57 # learnt constraints : 41648 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 200325 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 6 # Number of update (reduction) of LBD : 20544 # 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) : 2424360.977534823 # non guided choices 268652 # learnt constraints type # Solving done (72.949s). # The solution found IS optimal # Solution contains:1121