# Solver launched on Mon Sep 03 06:46:33 UTC 2012 # Using input file /home/competition/data/upgrade/difficult/rand869.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/trendy-size/upgrade/difficult/rand869.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:7037 # Parsing done (7.041s). # Solving ... # Request size: 1027 # Number of packages after slice: 13256 # Slice efficiency: 85% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@64482923 # 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 18053 to 19003 # criteria sum(installedsize) size is 0 Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 0 using new vars 19003 to 19003 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 0 using new vars 19003 to 19003 # criteria new size is 4412 using new vars 19003 to 23415 # p cnf 23414 122757 # Current objective function value: 31(1.572s) # Current objective function value: 30(2.568s) # Current objective function value: 29(2.965s) # Current objective function value: 28(3.154s) # Current objective function value: 27(3.352s) # Current objective function value: 26(3.505s) # Found optimal criterion number 1 # Found optimal criterion number 2 # Current objective function value: 0(3.52s) # Found optimal criterion number 3 # Current objective function value: 0(4.213s) # Found optimal criterion number 4 # Current objective function value: 313(4.537s) # Current objective function value: 216(4.991s) # Current objective function value: 210(5.411s) # Current objective function value: 176(5.692s) # Current objective function value: 175(8.581s) # cleaning 3256 clauses out of 6511 with flag 16416/7145 # cleaning 4624 clauses out of 9248 with flag 35417/13144 # Current objective function value: 174(24.341s) # Current objective function value: 173(24.878s) # Current objective function value: 172(24.99s) # Current objective function value: 171(25.082s) # Current objective function value: 170(25.265s) # Current objective function value: 169(26.4s) # cleaning 5656 clauses out of 11312 with flag 2846/19840 # Current objective function value: 168(28.142s) # Current objective function value: 167(28.203s) # Found optimal solution for the last criterion # -removed criteria value: 26 # Removed packages: [abiword-gnome, aptitude, capplets, gdm, gnome, gnome-core, gnome-desktop-environment, gnome-office, kde, kdemultimedia, kdepim, libarts1-mpeglib, liblablgtk2-ocaml-dev, libnautilus2-2, libpanel-applet2-dev, libperl5.8, libxklavier8, linux-kernel-headers, mpeglib, nautilus, nautilus-cd-burner, nautilus-data, nautilus-media, tasksel, xlibs, xlibs-data] # -sum(installedsize) criteria value: 0 # -new criteria value: 167 # Newly installed packages: [dbus, debian-archive-keyring, fontconfig-config, gcc-4.4-base, gconf2-common, gij-3.3, globus-gsi-proxy-ssl-dbg, gnome-menus, grmonitor, gstreamer0.10-alsa, knetfilter, libaa1, libasyncns0, libavahi-client-dev, libavahi-client3, libavahi-common-data, libavahi-common-dev, libavahi-common3, libavahi-glib-dev, libavahi-glib1, libc-bin, libc-dev-bin, libcaca0, libcairo2, libcairo2-dev, libcamel1.2-8, libcap2, libcdio10, libcups2, libdatrie1, libdb4.4, libdb4.6, libdb4.8, libdbus-1-3, libdbus-1-dev, libdbus-glib-1-2, libdirectfb-1.2-9, libdvdnav4, libdvdread4, libebook1.2-5, libecal1.2-6, libedataserver1.2-7, libedataserverui1.2-6, libflac8, libfs6, libgcj-common, libgcj4, libglobus-gsi-proxy-ssl1, libglobus-openssl, libgnome-menu2, libgnome-window-settings1, libgnutls13, libgnutls26, libgomp1, libgraphicsmagick3, libgssapi-krb5-2, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtop2-7, libgtop2-common, libhal-storage1, libhal1, libiso9660-7, libjack0, libjasper1, libk5crypto3, libkeyutils1, libkrb5-3, libkrb5support0, libltdl7, libmodplug1, libmpcdec6, libnautilus-extension1, libncursesw5, libnotify1, libnspr4-0d, libnss3-0d, libpcrecpp0, libperl5.10, libpixman-1-0, libpixman-1-dev, libpthread-stubs0, libpthread-stubs0-dev, libpulse0, libreadline6, libselinux1-dev, libsensors-dev, libsepol1, libsepol1-dev, libslang2, libsndfile1, libsnmp-dev, libsnmp-perl, libsnmp15, libsqlite3-0, libssl0.9.8, libstdc++6, libsvm3-java, libsysfs2, libtasn1-3, libthai-data, libthai0, libtotem-plparser1, libts-0.0-0, libv4l-0, libvcdinfo0, libvte9, libwavpack1, libwnck18, libwrap0-dev, libx11-data, libxau-dev, libxau6, libxcb-render-util0, libxcb-render-util0-dev, libxcb-render0, libxcb-render0-dev, libxcb-shape0, libxcb-shm0, libxcb-xv0, libxcb1, libxcb1-dev, libxcomposite-dev, libxcomposite1, libxdamage-dev, libxdamage1, libxdmcp-dev, libxdmcp6, libxfixes-dev, libxfixes3, libxine1-bin, libxine1-console, libxine1-misc-plugins, libxine1-x, libxinerama-dev, libxinerama1, libxkbfile1, libxklavier10, libxmltok1, libxres1, libxss1, libxvmc1, libxxf86dga1, libxxf86misc1, libxxf86vm1, linux-libc-dev, lsb-base, lzma, metacity-common, python-gmenu, python-minimal, python-support, python2.6, python2.6-minimal, readline-common, x11-common, x11proto-composite-dev, x11proto-core-dev, x11proto-damage-dev, x11proto-fixes-dev, x11proto-input-dev, x11proto-kb-dev, x11proto-randr-dev, x11proto-xext-dev, x11proto-xinerama-dev, xkb-data-legacy, xtrans-dev] # starts : 35 # conflicts : 20999 # decisions : 1257893 # propagations : 32612546 # inspects : 79291228 # shortcuts : 0 # learnt literals : 90 # learnt binary clauses : 922 # learnt ternary clauses : 189 # learnt constraints : 20907 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 517538 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 3 # Number of update (reduction) of LBD : 5676 # 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) : 1131201.734304544 # non guided choices 888379 # learnt constraints type # Solving done (33.584s). # The solution found IS optimal # Solution contains:1091