# Solver launched on Mon Sep 03 06:33:45 UTC 2012 # Using input file /home/competition/data/upgrade/easy/rand377.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/trendy-size/upgrade/easy/rand377.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:6377 # Parsing done (6.383s). # Solving ... # Request size: 1012 # Number of packages after slice: 8060 # 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 11249 to 12199 # criteria sum(installedsize) size is 0 Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 0 using new vars 12199 to 12199 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 0 using new vars 12199 to 12199 # criteria new size is 2913 using new vars 12199 to 15112 # p cnf 15111 74239 # Current objective function value: 63(1.463s) # Current objective function value: 62(1.926s) # Current objective function value: 49(2.244s) # Current objective function value: 44(2.366s) # Current objective function value: 43(2.455s) # Current objective function value: 42(2.554s) # Current objective function value: 41(2.71s) # Current objective function value: 38(2.784s) # Current objective function value: 37(2.823s) # Found optimal criterion number 1 # Found optimal criterion number 2 # Current objective function value: 0(2.846s) # Found optimal criterion number 3 # Current objective function value: 0(3.174s) # Found optimal criterion number 4 # Current objective function value: 248(3.403s) # Current objective function value: 225(3.662s) # Current objective function value: 188(3.778s) # Current objective function value: 184(3.839s) # Current objective function value: 182(3.908s) # Current objective function value: 179(3.944s) # Found optimal solution for the last criterion # -removed criteria value: 37 # Removed packages: [capplets, dbus-1, dbus-glib-1, exim4, gnome, gnome-desktop-environment, hotplug, kamera, kde, kde-amusements, kdeedu, kdegames, kdegraphics, kdeutils, kig, kjots, kpoker, libboost-python1.32.0, libdps1, libexif10, libhal-storage0, libhal0, libmagick6, libmodplug0, libnautilus-burn0, libnautilus2-2, libxft1, libxklavier8, linux-kernel-headers, nautilus-media, python2.3, python2.3-gtk2, python2.3-numeric, xfree86-common, xlibmesa-glu-dev, xlibs, xserver-common] # -sum(installedsize) criteria value: 0 # -new criteria value: 179 # Newly installed packages: [apache2-utils, apache2.2-common, bittorrent, cdrdao, dbus, dvd+rw-tools, eject, fontconfig-config, gcc-4.3-base, gconf2-common, genisoimage, gnome-cards-data, gnome-menus, gnome-mount, gstreamer0.10-alsa, liba52-0.7.4, libaa1, libalgorithm-diff-perl, libavahi-client-dev, libavahi-client3, libavahi-common-data, libavahi-common-dev, libavahi-common3, libavahi-glib-dev, libavahi-glib1, libavcodec0d, libcairo2, libcairo2-dev, libcamel1.2-8, libcgi-session-perl, libcups2, libdatrie0, libdb4.4, libdbus-1-3, libdbus-1-dev, libdbus-glib-1-2, libdigest-sha1-perl, libdirectfb-1.0-0, libdirectfb-dev, libdirectfb-extra, libdrm2, libebook1.2-5, libecal1.2-6, libedataserver1.2-7, libedataserverui1.2-6, libeel2-2.14, liberror-perl, libexif12, libfontenc-dev, libfontenc1, libfs6, libgl1-mesa-dev, libgl1-mesa-dri, libgl1-mesa-glx, libglu1-mesa, libglu1-mesa-dev, libgnome-menu2, libgnome-window-settings1, libgnutls13, libgnutls26, libgoffice-1-2, libgoffice-1-common, libgsf-1-114, libgsf-1-common, libgsf-gnome-1-114, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtop2-7, libgtop2-common, libhal-storage1, libhal1, libkeyutils1, liblocale-maketext-lexicon-perl, libmagick9, libmodplug0c2, libmpeg3-1, libmpeg3-dev, libnautilus-burn3, libnautilus-extension1, libncursesw5, libnotify1, libnspr4-0d, libnss3-0d, libpcrecpp0, libpixman-1-0, libpixman-1-dev, libpostproc0d, libpthread-stubs0, libpthread-stubs0-dev, libselinux1-dev, libsepol1, libsepol1-dev, libslang2, libssl0.9.8, libstdc++6, libsysfs-dev, libsysfs2, libtasn1-3, libtext-diff-perl, libthai-data, libthai0, libtotem-plparser1, libts-0.0-0, libvolume-id0, libwnck18, libx11-data, libxau-dev, libxau6, libxcb-render-util0, libxcb-render-util0-dev, libxcb-render0, libxcb-render0-dev, libxcb1, libxcb1-dev, libxcomposite-dev, libxcomposite1, libxdamage-dev, libxdamage1, libxdmcp-dev, libxdmcp6, libxfixes-dev, libxfixes3, libxfont-dev, libxfont1, libxinerama-dev, libxinerama1, libxkbfile1, libxklavier10, libxmu-headers, libxres1, libxss1, libxvmc1, libxxf86dga1, libxxf86misc1, libxxf86vm1, linux-libc-dev, lsb-base, mesa-common-dev, metacity-common, packeth, pcrd, python-cairo, python-central, python-glade2, python-gmenu, python-minimal, python-numeric, python-support, python2.4, python2.4-minimal, rcs, readline-common, tcl8.3, twiki, vbox3, wodim, x11-common, x11proto-composite-dev, x11proto-core-dev, x11proto-damage-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, xbitmaps, xcursor-themes, xfonts-encodings, xfonts-utils, xkb-data-legacy, xserver-xorg, xserver-xorg-core, xserver-xorg-input-void, xserver-xorg-video-vmware, xtrans-dev, xutils-dev] # starts : 20 # conflicts : 2393 # decisions : 635156 # propagations : 9057945 # inspects : 19145356 # shortcuts : 0 # learnt literals : 121 # learnt binary clauses : 418 # learnt ternary clauses : 67 # learnt constraints : 2270 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 1716 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 0 # Number of update (reduction) of LBD : 1020 # 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) : 1066142.3022598869 # non guided choices 413004 # learnt constraints type # Solving done (13.619s). # The solution found IS optimal # Solution contains:1092