# Solver launched on Mon Sep 03 06:41:22 UTC 2012 # Using input file /home/competition/data/upgrade/difficult/rand172.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/trendy-size/upgrade/difficult/rand172.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:7649 # Parsing done (7.655s). # Solving ... # Request size: 1027 # Number of packages after slice: 13238 # 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 18035 to 18985 # criteria sum(installedsize) size is 0 Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 0 using new vars 18985 to 18985 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 0 using new vars 18985 to 18985 # criteria new size is 4404 using new vars 18985 to 23389 # p cnf 23388 122603 # Current objective function value: 76(1.024s) # Current objective function value: 74(1.511s) # Current objective function value: 73(2.045s) # Current objective function value: 72(2.317s) # Current objective function value: 67(2.505s) # Current objective function value: 66(2.766s) # Current objective function value: 65(2.848s) # Found optimal criterion number 1 # Found optimal criterion number 2 # Current objective function value: 0(2.888s) # Found optimal criterion number 3 # Current objective function value: 0(3.554s) # Found optimal criterion number 4 # Current objective function value: 568(3.884s) # Current objective function value: 485(4.235s) # Current objective function value: 483(4.535s) # Current objective function value: 290(4.777s) # Current objective function value: 289(4.967s) # Current objective function value: 284(5.106s) # cleaning 3130 clauses out of 6273 with flag 22268/6980 # cleaning 4572 clauses out of 9143 with flag 46788/12980 # cleaning 5781 clauses out of 11571 with flag 79177/19980 # cleaning 6891 clauses out of 13790 with flag 117187/27980 # cleaning 7921 clauses out of 15897 with flag 147739/36980 # cleaning 8988 clauses out of 17976 with flag 182917/46980 # cleaning 9985 clauses out of 19989 with flag 221677/57981 # cleaning 10993 clauses out of 22004 with flag 266209/69981 # cleaning 12003 clauses out of 24012 with flag 319520/82982 # cleaning 12998 clauses out of 26006 with flag 365472/96980 # Solver timed out after 285.081s) # -removed criteria value: 65 # Removed packages: [aptitude, capplets, gnome, gnome-desktop-environment, gnome-gv, kde, kde-amusements, kde-core, kde-devel, kde-devel-extras, kdeaddons, kdebase, kdebase-dev, kdebase-kio-plugins, kdegames, kdelibs, kdelibs4-dev, kdesdk, kdevelop3, kdevelop3-data, kdevelop3-plugins, klickety, knewsticker-scripts, konq-plugins, konqueror, kspy, libarts1-dev, libbonoboui2-dev, libegroupwise6, libglade2-dev, libgnomecanvas2-dev, libgnomeui-dev, libgnutls11, libgnutls11-dev, libgtk1.2-dev, libgtk2.0-dev, libgtkgl2.0-dev, libgtkspell-dev, libkonq4-dev, liblablgtk2-ocaml-dev, libldap2, liblzo1, libmlgtk-ocaml-dev, libnautilus2-2, libnews-nntpclient-perl, libopenh323-1.15.2, libpanel-applet2-dev, libpt-1.8.3, libpt-plugins-oss, libpt-plugins-v4l2, libqt3-mt-dev, librsvg2-dev, libsoup2.2-7, libsvn0, libtasn1-2-dev, libxext-dev, libxi-dev, libxklavier8, libxmu-dev, libxrandr-dev, libxv-dev, linux-kernel-headers, nautilus-media, rhythmbox, tasksel] # -sum(installedsize) criteria value: 0 # -new criteria value: 284 # Newly installed packages: [bsdgames, ca-certificates, cdrdao, comerr-dev, dbus, dbus-x11, debian-archive-keyring, dvd+rw-tools, ekiga, evolution-common, evolution-data-server-common, fontconfig-config, gcc-4.4-base, gconf2-common, genisoimage, gnome-cards-data, gnome-doc-utils, gnome-media-common, gnome-menus, gnome-settings-daemon, gpgv, gstreamer0.10-alsa, gstreamer0.10-plugins-base, gstreamer0.10-plugins-good, gtk2-engines, gtkhtml3.14, guile-1.8-libs, industrial-cursor-theme, install-info, iso-codes, krb5-multidev, libaa1, libasyncns0, libavahi-client-dev, libavahi-client3, libavahi-common-data, libavahi-common-dev, libavahi-common3, libavahi-glib-dev, libavahi-glib1, libavc1394-0, libbluetooth2, libc-bin, libc-dev-bin, libcaca0, libcairo2, libcairo2-dev, libcamel1.2-11, libcap2, libcdio10, libcdio6, libcucul0, libcups2, libcups2-dev, libcupsys2, libcurl3-gnutls, libdatrie1, libdb4.6, libdb4.8, libdbd-mysql-perl, libdbi-perl, libdbus-1-3, libdbus-1-dev, libdbus-glib-1-2, libdirectfb-1.2-9, libdmx1, libdrm2, libdv4, libdvdnav4, libdvdread4, libebook1.2-9, libecal1.2-7, libedata-book1.2-2, libedata-cal1.2-6, libedataserver1.2-9, libedataserverui1.2-8, libeel2-2.14, libegroupwise1.2-13, libelfg0, libepc-1.0-1, libepc-ui-1.0-1, libexchange-storage1.2-3, libexif12, libflac7, libflac8, libfontenc-dev, libfontenc1, libgail18, libgalago3, libgdata-google1.2-1, libgdata1.2-1, libgl1-mesa-dev, libgl1-mesa-dri, libgl1-mesa-glx, libgmp3c2, libgmyth0, libgnome-media0, libgnome-menu2, libgnome-window-settings1, libgnomekbd-common, libgnomekbd2, libgnomekbdui2, libgnutls-dev, libgnutls26, libgoffice-1-2, libgoffice-1-common, libgomp1, libgraphicsmagick3, libgsasl7, libgsf-1-114, libgsf-1-common, libgsf-gnome-1-114, libgssapi-krb5-2, libgssrpc4, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtkhtml3.14-19, libgtop2-7, libgtop2-common, libhal-storage1, libhal1, libiec61883-0, libiso9660-7, libjack0, libjasper1, libk5crypto3, libkadm5clnt-mit7, libkadm5srv-mit7, libkdb5-4, libkeyutils1, libkpathsea4, libkrb5-3, libkrb5-dev, libkrb5support0, libldap-2.4-2, libltdl3, libltdl7, liblzma2, libmailutils1, libmodplug1, libmozjs0d, libmpcdec6, libmysqlclient12, libmysqlclient15off, libmysqlclient16, libnautilus-burn3, libnautilus-extension1, libncursesw5, libnet-daemon-perl, libnettle3, libnm-glib0, libnotify1, libnspr4-0d, libnss3-0d, libnss3-1d, libntlm0, liboil0.3, libopal-2.2, libpcrecpp0, libpisock9, libpisync1, libpixman-1-0, libpixman-1-dev, libplrpc-perl, libpoppler0c2, libpt-1.10.10, libpt-1.10.10-plugins-oss, libpt-1.10.10-plugins-v4l2, libpth20, libpthread-stubs0, libpthread-stubs0-dev, libpulse0, libraw1394-8, libreadline6, libroxen-explaindir, libsasl2-2, libselinux1-dev, libsepol1, libsepol1-dev, libslab0, libslang2, libsndfile1, libsoup2.4-1, libspeexdsp1, libsqlite3-0, libssl0.9.8, libstdc++6, libsysfs2, libtag1-vanilla, libtag1c2a, libtalloc2, libtasn1-3, libtasn1-3-dev, libtext-shellwords-perl, libthai-data, libthai0, libtotem-plparser10, libtrackerclient0, libts-0.0-0, libv4l-0, libvcdinfo0, libvisual-0.4-0, libvte9, libwavpack1, libwbclient0, libwnck18, libwnck22, 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, libxcomposite1, libxdamage1, libxdmcp-dev, libxdmcp6, libxfixes3, libxfont-dev, libxfont1, libxine1-bin, libxine1-console, libxine1-misc-plugins, libxine1-x, libxinerama1, libxkbfile1, libxklavier10, libxklavier12, libxres1, libxss1, libxul-common, libxul0d, libxvmc1, libxxf86misc1, libxxf86vm1, linux-libc-dev, lsb-base, mailutils-mh, mesa-common-dev, metacity-common, mysql-client-5.0, mysql-common, mysql-server-5.0, openssl, pike7.6-core, pike7.6-image, pike7.6-mysql, python-gdata, python-gmenu, python-libxml2, python-minimal, python-support, python2.5, python2.5-minimal, python2.6, python2.6-minimal, readline-common, roxen4, tex-common, totem-common, totem-plugins, unzip, wmpuzzle, wodim, wswiss, x11-common, x11proto-core-dev, x11proto-fonts-dev, x11proto-input-dev, x11proto-kb-dev, xbitmaps, xcursor-themes, xkb-data-legacy, xsltproc, xtrans-dev, xz-lzma, xz-utils, zip] # starts : 84 # conflicts : 110227 # decisions : 2675693 # propagations : 474392725 # inspects : 1087566003 # shortcuts : 0 # learnt literals : 39 # learnt binary clauses : 772 # learnt ternary clauses : 178 # learnt constraints : 110187 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 1692134 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 10 # Number of update (reduction) of LBD : 24600 # 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) : 1664384.0386491057 # non guided choices 926598 # learnt constraints type # org.sat4j.minisat.constraints.cnf.LearntBinaryClause => 424 # org.sat4j.minisat.constraints.cnf.LearntWLClause => 25831 # Solving done (289.748s). # WARNING: The solution found MIGHT NOT BE optimal # Solution contains:1169