# Solver launched on Mon Sep 03 06:45:00 UTC 2012 # Using input file /home/competition/data/upgrade/difficult/rand794.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/trendy-size/upgrade/difficult/rand794.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:7563 # Parsing done (7.569s). # Solving ... # Request size: 1027 # Number of packages after slice: 13279 # 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 18087 to 19037 # criteria sum(installedsize) size is 0 Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 0 using new vars 19037 to 19037 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 0 using new vars 19037 to 19037 # criteria new size is 4416 using new vars 19037 to 23453 # p cnf 23452 122919 # Current objective function value: 55(1.67s) # Current objective function value: 52(2.309s) # Current objective function value: 50(2.649s) # Found optimal criterion number 1 # Found optimal criterion number 2 # Current objective function value: 0(2.77s) # Found optimal criterion number 3 # Current objective function value: 0(3.515s) # Found optimal criterion number 4 # Current objective function value: 229(3.937s) # Current objective function value: 213(4.251s) # Current objective function value: 193(4.538s) # Current objective function value: 189(4.738s) # cleaning 2587 clauses out of 5174 with flag 16130/5603 # Current objective function value: 188(26.918s) # Current objective function value: 187(28.19s) # Current objective function value: 186(28.267s) # Current objective function value: 185(28.632s) # Current objective function value: 184(28.896s) # Current objective function value: 183(29.339s) # Found optimal solution for the last criterion # -removed criteria value: 50 # Removed packages: [abiword-gnome, gdm, gnome, gnome-desktop-environment, gnumeric, gpdf, gtkhtml3.2, iputils-ping, kde, kde-devel, kde-devel-extras, kdebase-dev, kdegraphics, kdelibs4-dev, kdesdk, kdvi, kspy, libarts1-dev, libbonoboui2-dev, libenchant1, libgal2.2-1, libgal2.2-common, libgc1, libglade2-dev, libglibmm-2.4-1, libgnomecanvas2-dev, libgnomeprint2.2-0, libgnomeprint2.2-data, libgnomeprintui2.2-0, libgnomeui-dev, libgtk2.0-dev, libgtkgl2.0-dev, libgtkhtml3.2-11, libgtkmm-2.4-1, libgtksourceview1.0-0, libgtkspell-dev, libkonq4-dev, liblablgtk2-ocaml-dev, libpanel-applet2-dev, libpango1.0-dev, libqt3-mt-dev, librsvg2-dev, libsigc++-2.0-0, libstlport4.6, libxft-dev, linux-kernel-headers, openoffice.org, openoffice.org-bin, openoffice.org-debian-files, python2.3-gtk2] # -sum(installedsize) criteria value: 0 # -new criteria value: 183 # Newly installed packages: [ca-certificates, dbus, dbus-x11, debian-archive-keyring, dropbear, evolution-common, evolution-data-server-common, fontconfig-config, gauche, gauche-gl, gcc-4.4-base, gconf2-common, git, gitolite, gnome-cards-data, gnome-menus, gtk2-engines, gtkhtml3.14, industrial-cursor-theme, inetutils-ping, iso-codes, libaa1, libatlas3gf-sse2, libavahi-client-dev, libavahi-client3, libavahi-common-data, libavahi-common-dev, libavahi-common3, libavahi-glib-dev, libavahi-glib1, libbabl-0.0-0, libbluetooth2, libc-bin, libc-dev-bin, libcairo2, libcairomm-1.0-1, libcamel1.2-11, libcreal-ocaml-dev, libcups2, libcurl3-gnutls, libcwidget3, libdatrie1, libdb4.6, libdb4.8, libdbus-1-3, libdbus-1-dev, libdbus-glib-1-2, libebook1.2-9, libecal1.2-7, libedata-book1.2-2, libedata-cal1.2-6, libedataserver1.2-9, libedataserverui1.2-8, libegroupwise1.2-13, libenchant1c2a, libept0, liberror-perl, libexchange-storage1.2-3, libexif12, libffi5, libgail18, libgc1c2, libgdata-google1.2-1, libgdata1.2-1, libgegl-0.0-0, libgfortran3, libglibmm-2.4-1c2a, libgmp-ocaml, libgmp-ocaml-dev, libgmp3, libgmp3-dev, libgnome-menu2, libgnutls26, libgomp1, libgsf-1-114, libgsf-1-common, libgsl0ldbl, libgssapi-krb5-2, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtkhtml3.14-19, libgtkmm-2.4-1c2a, libgtksourceview2.0-0, libgtksourceview2.0-common, libgudev-1.0-0, libhal-storage1, libhal1, libhtml-popuptreeselect-perl, libhunspell-1.2-0, libhyphen0, libicu38, libicu44, libilmbase6, libjasper1, libk5crypto3, libkeyutils1, libkrb5-3, libkrb5support0, libldap-2.4-2, liblqr-1-0, libltdl7, libmagick++3, libmagickcore3, libmagickwand3, libncursesw5, libneon27, libnm-glib0, libnotify1, libnspr4-0d, libnss3-1d, libopenexr6, libopenjpeg2, libopenraw1, libpangomm-1.4-1, libpcrecpp0, libpisock9, libpisync1, libpixman-1-0, libpoppler-glib4, libpoppler5, libpython2.6, libreadline6, libsasl2-2, libselinux1-dev, libsepol1, libsepol1-dev, libsigc++-2.0-0c2a, libslang2, libsoup2.4-1, libsqlite3-0, libssh2-1, libssl0.9.8, libstdc++6, libstlport4.6ldbl, libtasn1-3, libthai-data, libthai0, libudev0, libvte9, libwebkit-1.0-2, libwebkit-1.0-common, libwnck22, libwpd8c2a, libwpg-0.1-1, libxapian15, libxau6, libxcb-render-util0, libxcb-render0, libxcb1, libxcomposite1, libxdamage1, libxdmcp6, libxfixes3, libxinerama1, libxres1, linux-libc-dev, lsb-base, lzma, mailman, nginx, openoffice.org-common, openoffice.org-core, openoffice.org-gnome, openoffice.org-gtk, openoffice.org-style-andromeda, openoffice.org-style-tango, openssl, pwgen, python-cairo, python-gmenu, python-gobject, python-gtksourceview2, python-minimal, python-numpy, python-support, python2.6, python2.6-minimal, readline-common, simple-scan, x11-common, x11proto-core-dev, x11proto-randr-dev, xdg-utils] # starts : 25 # conflicts : 11475 # decisions : 945816 # propagations : 33976607 # inspects : 79211797 # shortcuts : 0 # learnt literals : 185 # learnt binary clauses : 382 # learnt ternary clauses : 78 # learnt constraints : 11288 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 33631 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 1 # Number of update (reduction) of LBD : 2841 # 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) : 1149450.488852803 # non guided choices 613525 # learnt constraints type # Solving done (35.387s). # The solution found IS optimal # Solution contains:1083