# Solver launched on Mon Sep 03 06:46:27 UTC 2012 # Using input file /home/competition/data/upgrade/difficult/rand874.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/trendy-size/upgrade/difficult/rand874.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:7022 # Parsing done (7.028s). # Solving ... # Request size: 1027 # Number of packages after slice: 13281 # 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 18096 to 19046 # criteria sum(installedsize) size is 0 Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 0 using new vars 19046 to 19046 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 0 using new vars 19046 to 19046 # criteria new size is 4426 using new vars 19046 to 23472 # p cnf 23471 123034 # Current objective function value: 59(1.212s) # Current objective function value: 58(1.9s) # Current objective function value: 30(2.345s) # Found optimal criterion number 1 # Found optimal criterion number 2 # Current objective function value: 0(2.432s) # Found optimal criterion number 3 # Current objective function value: 0(3.113s) # Found optimal criterion number 4 # Current objective function value: 460(3.598s) # Current objective function value: 254(4.057s) # Current objective function value: 239(4.318s) # Current objective function value: 238(7.829s) # Current objective function value: 230(7.974s) # Current objective function value: 229(8.064s) # Current objective function value: 228(18.201s) # Current objective function value: 225(18.235s) # cleaning 3551 clauses out of 7105 with flag 14604/7715 # Current objective function value: 224(36.19s) # Current objective function value: 223(37.431s) # Current objective function value: 222(37.453s) # Current objective function value: 221(43.939s) # cleaning 5257 clauses out of 10513 with flag 7198/14674 # Current objective function value: 220(63.389s) # cleaning 5148 clauses out of 10295 with flag 2573/19713 # Current objective function value: 219(73.996s) # Current objective function value: 217(74.026s) # Current objective function value: 216(80.646s) # cleaning 5395 clauses out of 10792 with flag 2799/25358 # cleaning 5697 clauses out of 11393 with flag 24079/31358 # Current objective function value: 215(113.279s) # cleaning 5688 clauses out of 11375 with flag 12088/37037 # Current objective function value: 214(141.27s) # Current objective function value: 213(146.311s) # Current objective function value: 212(146.347s) # Current objective function value: 211(149.953s) # Current objective function value: 209(149.98s) # cleaning 6632 clauses out of 13264 with flag 2419/44614 # Found optimal solution for the last criterion # -removed criteria value: 30 # Removed packages: [akode, gdm, gnome, gnome-desktop-environment, gnome-utils, kcmlinuz, kde, kde-amusements, kdeedu, kdelibs4, kdevelop3-data, kdevelop3-plugins, kig, kmessedwords, libarts1, libjack0.80.0-dev, libkcal2a, libkdeedu1, libkdenetwork2, libkdepim1, libkleopatra0a, libmimelib1a, libqt3c102-mt, libvorbis-ocaml-dev, linux-kernel-headers, secpolicy, vimpart, x-window-system-core, xfonts-75dpi, xserver-common] # -sum(installedsize) criteria value: 0 # -new criteria value: 209 # Newly installed packages: [akregator, binfmt-support, ca-certificates, comerr-dev, eject, fontconfig-config, gcc-4.4-base, indi, kalzium-data, kdebase-bin-kde3, kdeeject, kdelibs4c2a, kdepim-kresources, kdevelop, kdevelop-data, knetworkconf, lib64gomp1, lib64gomp1-dbg, libaa1, libacl1-dev, libakode2, libarts1-akode, libarts1c2a, libasyncns0, libattr1-dev, libavahi-client-dev, libavahi-client3, libavahi-common-data, libavahi-common-dev, libavahi-common3, libavahi-compat-libdnssd1, libavahi-qt3-1, libavahi-qt3-dev, libbluetooth2, libc-bin, libc-dev-bin, libc6-amd64, libcaca0, libcairo2, libcairo2-dev, libcap2, libcdio10, libclucene0ldbl, libcups2, libcups2-dev, libcurl3-gnutls, libdb4.3, libdb4.6, libdb4.6++, libdb4.8, libdbus-1-3, libdbus-1-dev, libdbus-qt-1-1c2, libdirectfb-1.2-9, libdvdnav4, libdvdread4, libedit2, libexif12, libexiv2-9, libflac8, libfontenc1, libfs6, libgmp3c2, libgnokii3, libgnutls26, libgomp1, libgraphicsmagick3, libgsmme1c2a, libgstreamer0.10-0, libhal-storage1, libhal1, libilmbase-dev, libilmbase6, libindex0, libiodbc2, libiso9660-7, libiw29, libjack0, libjack0.100.0-0, libjack0.100.0-dev, libjasper-dev, libjasper1, libkadm55, libkcal2b, libkdcraw-dev, libkdcraw3, libkdecore5, libkdeedu3, libkdepim1a, libkdeui5, libkeyutils1, libkio5, libkiten1, libkjsapi4, libkjsembed4, libkleopatra1, libkmime2, libkparts4, libkrb5-dev, libkrosscore4, libktnef1, libldap-2.4-2, liblockdev1, libltdl7, liblua50, liblua50-dev, liblualib50, liblualib50-dev, liblzma2, libmeanwhile1, libmimelib1c2a, libmodplug1, libmpcdec6, libncursesw5, libopenexr-dev, libopenexr6, libparportled, libpcrecpp0, libpisock9, libpoppler-qt2, libpoppler3, libpulse0, libqt3-mt, libqt4-dbus, libqt4-network, libqt4-script, libqt4-svg, libqt4-xml, libqtcore4, libqtgui4, libraptor1, librasqal2, libraw1394-8, librdf0, libsasl2-2, libsasl2-dev, libsasl2-modules, libsensors4, libslang2, libsndfile1, libsnmp9, libsolid4, libsoprano4, libssl0.9.8, libstdc++6, libstreamanalyzer0, libstreams0, libsysfs2, libtag1-vanilla, libtag1c2a, libtasn1-3, libtiff4-dev, libtiffxx0c2, libts-0.0-0, libv4l-0, libvcdinfo0, libwavpack1, libxau6, libxcb-shape0, libxcb-shm0, libxcb-xv0, libxcb1, libxcomposite1, libxdamage1, libxdmcp6, libxfixes3, libxfont1, libxine1-bin, libxine1-console, libxine1-misc-plugins, libxine1-x, libxinerama-dev, libxinerama1, libxkbfile1, libxslt1-dev, libxss1, libxvmc1, libxxf86dga1, libxxf86misc1, libxxf86vm1, linux-libc-dev, llvm, llvm-dev, llvm-gcc-4.2, lsb-base, lua50, networkstatus, openssh-blacklist, openssh-client, openssh-server, openssl, oss-compat, perl-suid, qemu-user, soprano-daemon, ttf-dustin, ttf-kochi-mincho, wireless-tools, x11-common, x11-xserver-utils, x11proto-core-dev, x11proto-randr-dev, x11proto-xinerama-dev, xauth, xkb-data, xserver-xorg, xserver-xorg-core, xserver-xorg-input-void, xserver-xorg-video-voodoo] # starts : 61 # conflicts : 48065 # decisions : 1525855 # propagations : 267295234 # inspects : 635406660 # shortcuts : 0 # learnt literals : 147 # learnt binary clauses : 638 # learnt ternary clauses : 127 # learnt constraints : 47916 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 62474 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 7 # Number of update (reduction) of LBD : 24487 # 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) : 1606544.2994608695 # non guided choices 845146 # learnt constraints type # Solving done (170.223s). # The solution found IS optimal # Solution contains:1129