# Solver launched on Mon Sep 03 06:33:20 UTC 2012 # Using input file /home/competition/data/upgrade/easy/rand18.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/trendy-size/upgrade/easy/rand18.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:5616 # Parsing done (5.622s). # Solving ... # Request size: 1012 # Number of packages after slice: 8048 # Slice efficiency: 85% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@7e0c2ff5 # 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 11228 to 12178 # criteria sum(installedsize) size is 0 Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 0 using new vars 12178 to 12178 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 0 using new vars 12178 to 12178 # criteria new size is 2909 using new vars 12178 to 15087 # p cnf 15086 74196 # Current objective function value: 44(0.972s) # Current objective function value: 43(1.407s) # Current objective function value: 41(1.529s) # Current objective function value: 40(1.581s) # Current objective function value: 39(1.636s) # Current objective function value: 38(1.784s) # Found optimal criterion number 1 # Found optimal criterion number 2 # Current objective function value: 0(1.848s) # Found optimal criterion number 3 # Current objective function value: 0(2.038s) # Found optimal criterion number 4 # Current objective function value: 104(2.137s) # Current objective function value: 107(2.254s) # Current objective function value: 106(6.983s) # Current objective function value: 105(7.371s) # Current objective function value: 101(7.411s) # Current objective function value: 72(7.433s) # Current objective function value: 71(8.091s) # Current objective function value: 70(8.204s) # Current objective function value: 67(8.226s) # Current objective function value: 66(8.24s) # Found optimal solution for the last criterion # -removed criteria value: 38 # Removed packages: [capplets, gimp, gnome, gnome-applets, gnome-control-center, gnome-core, gnome-desktop-environment, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnome-terminal, kde, kde-amusements, kde-devel-extras, kdeedu, kdevelop3, kdevelop3-data, kdevelop3-plugins, kturtle, libdps1, libmagick6, libmlgtk-ocaml, libmlgtk-ocaml-dev, libsvn0, libvte-common, libvte4, libxft1, nautilus, nautilus-media, synaptic, totem, totem-xine, wget, xfree86-common, xlibmesa-glu-dev, xlibs, xserver-common] # -sum(installedsize) criteria value: 0 # -new criteria value: 66 # Newly installed packages: [fontconfig-config, freeglut3-dev, gcc, gcc-3.3, gcc-4.1-base, kernel-headers-2.4.27-3, kernel-headers-2.4.27-3-k7, libcairo2, libcairo2-dev, libconvert-uulib-perl, libdb4.4, libdrm2, libfontenc-dev, libfontenc1, libfs6, libgl1-mesa-dev, libgl1-mesa-dri, libgl1-mesa-glx, libglu1-mesa, libglu1-mesa-dev, libgocr-doc, liblablgtk2-gl-ocaml, liblablgtk2-gl-ocaml-dev, libmagick9, libperl6-export-perl, libperl6-slurp-perl, libx11-data, libxau-dev, libxau6, libxdmcp-dev, libxdmcp6, libxfixes-dev, libxfixes3, libxfont-dev, libxfont1, libxinerama-dev, libxinerama1, libxkbfile1, libxmu-headers, libxss1, libxxf86dga1, libxxf86vm1, lsb-base, mesa-common-dev, tzdata, x11-common, 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, xbitmaps, xcursor-themes, xfonts-encodings, xfonts-utils, xkb-data-legacy, xserver-xorg, xserver-xorg-core, xserver-xorg-input-void, xserver-xorg-video-voodoo, xtrans-dev, xutils-dev] # starts : 20 # conflicts : 2511 # decisions : 290366 # propagations : 9695485 # inspects : 22202963 # shortcuts : 0 # learnt literals : 34 # learnt binary clauses : 263 # learnt ternary clauses : 47 # learnt constraints : 2475 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 8442 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 0 # Number of update (reduction) of LBD : 852 # 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) : 1170952.2946859903 # non guided choices 200365 # learnt constraints type # Solving done (12.999s). # The solution found IS optimal # Solution contains:978