# Solver launched on Mon Sep 03 06:40:38 UTC 2012 # Using input file /home/competition/data/upgrade/easy/rand929.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/trendy-size/upgrade/easy/rand929.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:4656 # Parsing done (4.661s). # Solving ... # Request size: 1012 # Number of packages after slice: 8080 # 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 11267 to 12217 # criteria sum(installedsize) size is 0 Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 0 using new vars 12217 to 12217 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 0 using new vars 12217 to 12217 # criteria new size is 2925 using new vars 12217 to 15142 # p cnf 15141 74402 # Current objective function value: 63(1.098s) # Current objective function value: 62(1.441s) # Found optimal criterion number 1 # Found optimal criterion number 2 # Current objective function value: 0(1.502s) # Found optimal criterion number 3 # Current objective function value: 0(1.924s) # Found optimal criterion number 4 # Current objective function value: 212(2.126s) # Current objective function value: 235(2.35s) # Current objective function value: 216(2.5s) # Current objective function value: 198(2.658s) # Current objective function value: 194(2.736s) # cleaning 2600 clauses out of 5199 with flag 14101/5455 # cleaning 4307 clauses out of 8614 with flag 30027/11470 # Found optimal solution for the last criterion # -removed criteria value: 62 # Removed packages: [akode, apt-utils, capplets, gnome, gnome-applets, gnome-control-center, gnome-core, gnome-desktop-environment, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnome-terminal, kcmlinuz, kde, kde-devel, kde-devel-extras, kdeaddons, kdelibs-bin, kdelibs4, kdenetwork, kdesdk, kdesdk-scripts, kdevelop3-data, kdevelop3-plugins, kmessedwords, knewsticker-scripts, konq-plugins, kppp, libarts1, libbonoboui2-dev, libdps1, libglade2-dev, libgnome-keyring-dev, libgnomeui-dev, libjack0.80.0-0, libjack0.80.0-dev, libkcal2a, libkdeedu1, libkdenetwork2, libkdepim1, libkleopatra0a, liblablgtk2-ocaml-dev, libmagick6, libmimelib1a, libmodplug0, libpanel-applet2-dev, libqt3c102-mt, libtag1, libxft1, linux-kernel-headers, nautilus, nautilus-media, python, secpolicy, totem, totem-xine, vimpart, xfree86-common, xlibmesa-glu-dev, xlibs, xserver-common] # -sum(installedsize) criteria value: 0 # -new criteria value: 194 # Newly installed packages: [akregator, blinken, comerr-dev, eject, fontconfig-config, gcc-4.3-base, gcj-4.1-base, gij-4.1, indi, 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-qt3-1, libavahi-qt3-dev, libavc1394-0, libavcodec0d, libbluetooth2, libboost-python1.33.1, libcairo2, libcairo2-dev, libcdio-dev, libcdio7, libclass-accessor-perl, libcups2, libcups2-dev, libdb4.3, libdb4.6, libdb4.6++, libdbus-1-3, libdbus-1-dev, libdbus-qt-1-1c2, libdirectfb-0.9-25, libdrm2, libeasymock-java, libedit2, libemail-address-perl, libemail-messageid-perl, libemail-mime-contenttype-perl, libemail-mime-encodings-perl, libemail-mime-modifier-perl, libemail-mime-perl, libemail-simple-perl, libexif12, libflac8, libfontenc-dev, libfontenc1, libfreebob0, libfs6, libgcj-common, libgcj7-0, libgl1-mesa-dev, libgl1-mesa-dri, libgl1-mesa-glx, libglu1-mesa, libglu1-mesa-dev, libgmp3c2, libgnokii3, libgnutls26, libgsmme1c2a, libgstreamer0.10-0, libhal-storage1, libhal1, libhttp-recorder-perl, libhttp-request-params-perl, libiec61883-0, libilmbase-dev, libilmbase6, libindex0, libiso9660-5, libiso9660-dev, libiw29, libjack-dev, libjack0, libjack0.100.0-dev, libjasper-dev, libjasper1, libkadm55, libkcal2b, libkdeedu3, libkdepim1a, libkeyutils1, libkiten1, libkleopatra1, libkmime2, libkrb5-dev, libktnef1, libldap-2.4-2, liblockdev1, liblua50, liblua50-dev, liblualib50, liblualib50-dev, libmagick9, libmeanwhile1, libmime-types-perl, libmimelib1c2a, libmodplug0c2, libopenexr-dev, libopenexr6, libpcrecpp0, libpisock9, libpoppler-qt2, libpoppler3, libpostproc0d, libqt3-mt, libraw1394-8, libsasl2-2, libsasl2-dev, libsasl2-modules, libsensors4, libsnmp9, libssl0.9.8, libstdc++6, libsysfs2, libtag1c2a, libtasn1-3, libtiff4-dev, libtiffxx0c2, libx11-data, libxau-dev, libxau6, libxcomposite1, libxdamage1, libxdmcp-dev, libxdmcp6, libxfixes3, libxfont-dev, libxfont1, libxinerama-dev, libxinerama1, libxkbfile1, libxmu-headers, libxslt1-dev, libxss1, libxvmc1, libxxf86dga1, libxxf86misc1, libxxf86vm1, linux-libc-dev, lsb-base, lua50, mesa-common-dev, networkstatus, openssh-blacklist, openssh-client, openssh-server, oss-compat, perl-suid, python2.4, rkhunter, ttf-dustin, ttf-kochi-mincho, ttf-sjfonts, wireless-tools, x11-common, x11-xserver-utils, x11proto-core-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-legacy, xserver-xorg, xserver-xorg-core, xserver-xorg-input-void, xserver-xorg-video-nv, xtrans-dev, xutils-dev] # starts : 24 # conflicts : 15852 # decisions : 430838 # propagations : 58820715 # inspects : 118733515 # shortcuts : 0 # learnt literals : 124 # learnt binary clauses : 285 # learnt ternary clauses : 46 # learnt constraints : 15726 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 11542 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 2 # Number of update (reduction) of LBD : 6056 # 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) : 1848545.4116907604 # non guided choices 229684 # learnt constraints type # Solving done (37.066s). # The solution found IS optimal # Solution contains:1082