# Solver launched on Mon Sep 03 03:13:55 UTC 2012 # Using input file /home/competition/data/upgrade/easy/rand929.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/dist-upgrade/upgrade/easy/rand929.cudf.result # Objective function -notuptodate(solution),-aligned(solution,source,sourceversion),-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:5343 # Parsing done (5.37s). # Solving ... # Request size: 1012 # Number of packages after slice: 8080 # Slice efficiency: 85% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@5220be79 # 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:-notuptodate(solution),-aligned(solution,source,sourceversion),-unsat_recommends(solution),-count(new) Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 0 using new vars 11267 to 11267 # criteria aligned(source,sourceversion) size is 5806 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 5806 using new vars 11267 to 14171 # criteria new size is 2925 using new vars 14171 to 17096 # p cnf 17095 87101 # Found optimal criterion number 1 # Current objective function value: 13(1.455s) # Current objective function value: 6(1.639s) # cleaning 2557 clauses out of 5130 with flag 10574/5174 # cleaning 4279 clauses out of 8572 with flag 24301/11174 # cleaning 5641 clauses out of 11292 with flag 41062/18173 # cleaning 6824 clauses out of 13651 with flag 61678/26173 # cleaning 7905 clauses out of 15827 with flag 86598/35173 # cleaning 8951 clauses out of 17923 with flag 114272/45174 # cleaning 9978 clauses out of 19971 with flag 144717/56173 # cleaning 10993 clauses out of 21993 with flag 177150/68173 # cleaning 12001 clauses out of 24001 with flag 212788/81174 # cleaning 12996 clauses out of 26000 with flag 246354/95174 # cleaning 14002 clauses out of 28003 with flag 282693/110173 # cleaning 15000 clauses out of 30003 with flag 321215/126175 # cleaning 16001 clauses out of 32001 with flag 362286/143173 # cleaning 16996 clauses out of 34000 with flag 408670/161174 # cleaning 17999 clauses out of 36004 with flag 458175/180174 # cleaning 18995 clauses out of 38005 with flag 509963/200174 # cleaning 20001 clauses out of 40009 with flag 559302/221173 # cleaning 20995 clauses out of 42010 with flag 613218/243175 # cleaning 21998 clauses out of 44013 with flag 669182/266173 # cleaning 23001 clauses out of 46015 with flag 727295/290173 # cleaning 24006 clauses out of 48015 with flag 786076/315174 # cleaning 25004 clauses out of 50008 with flag 845975/341173 # cleaning 25995 clauses out of 52004 with flag 903972/368173 # cleaning 26999 clauses out of 54009 with flag 964573/396173 # cleaning 27998 clauses out of 56013 with flag 1027113/425176 # cleaning 29001 clauses out of 58012 with flag 1091428/455173 # cleaning 30004 clauses out of 60012 with flag 1158322/486174 # cleaning 31002 clauses out of 62009 with flag 1226001/518175 # Solver timed out after 285.155s) # -new criteria value: 505 # Newly installed packages: [9base, 9menu, a2ps, aewm, af, altgcc, app-install-data, aspell-es, aspell-ukr, blinken, bsh, busybox, ca-certificates, cdcd, cdebconf, cdrdao, chimera2, clamav-data, classpath-tools, cli-common, console-terminus, cpp-4.1, cramfsprogs, dash, debconf-english, debian-archive-keyring, devfsd, discover1-data, dmz-cursor-theme, doc-base, dsyslog, dvi2tty, dviutils, dwww, eject, epdfview, epos-ktd, epos-lpc, epos-ptd, esound-clients, fastjar, festival, festlex-cmu, festlex-poslex, festvox-kallpc16k, festvox-kdlpc8k, festvox-suopuhe-common, festvox-suopuhe-mv, fgetty, fontconfig-config, gamin, gawk, gcc-4.1-base, gcc-4.3-base, gcj-4.1-base, gij-4.1, gnome-audio, gnome-backgrounds, gnome-games-extra-data, gnustep-back, gnustep-base-common, gnustep-common, gnustep-gui-common, gnustep-ppd, gpgv, grep-dctrl, gtk2-engines, guile-1.6, hal-info, hardinfo, host, indi, industrial-cursor-theme, iproute, jikes, jwm, kalzium-data, kanagram, kbd, kdebase-bin-kde3, kdeeject, kdelibs4c2a, kdm, kgeography, kgeography-data, knetwalk, krb4-config, kterm, lapack3, larswm, latex-xcolor, ldso, libacr38u, libalut0, libao2, libapr1, libaprutil1, libarchive1, libarts1c2a, libasyncns0, libatm1, libavahi-client3, libavahi-common-data, libavahi-common3, libavahi-compat-libdnssd1, libavahi-qt3-1, libavc1394-0, libbcel-java, libbeecrypt6, libbinio1ldbl, libblas3gf, libboost-python1.34.1, libcairo-perl, libcairo2, libcairomm-1.0-1, libcanna1g, libcap2, libccid, libcdaudio1, libcddb2, libcdio-dev, libcdio3, libcitadel1, libclass-accessor-perl, libclucene0ldbl, libcolorblind0, libcompress-raw-zlib-perl, libcompress-zlib-perl, libcteco50000, libcups2, libcupsimage2, libcxxtools6, libdatrie0, libdb2, libdb4.4, libdb4.5, libdb4.6, libdbi-perl, libdbus-1-3, libdbus-glib-1-2, libdbus-qt-1-1c2, libdc1394-13, libdebian-installer4, libdevel-symdump-perl, libdigest-hmac-perl, libdigest-sha1-perl, libdirectfb-1.0-0, libdirectfb-extra, libdmx1, libdrm2, libeasymock-java, libeb12, libedit2, libefs1, libelfg0, libemail-address-perl, libemail-messageid-perl, libemail-mime-contenttype-perl, libemail-mime-encodings-perl, libemail-mime-modifier-perl, libemail-mime-perl, libemail-simple-perl, libept0, liberror-perl, libestools1.2, libetoken, libevtlog0, libexempi3, libexif12, libfaad0, libffcall1, libffi5, libfile-ncopy-perl, libfile-remove-perl, libfont-afm-perl, libfontenc1, libforms1, libfreebob0, libfreezethaw-perl, libfs6, libfsplib0, libg2c0, libgalago3, libgamin0, libgcj-common, libgcj7-0, libgcr410, libgd2-xpm, libgdome2-0, libgdome2-cpp-smart0c2a, libgecko2.0-cil, libgfortran3, libggz2, libgif4, libgl1-mesa-glide3, libglew1, libglib-perl, libglib2.0-cil, libglib2.0-data, libglide3, libglu1-mesa, libgmime2.1, libgmp3, libgnustep-base1.10, libgnustep-gui0.9, libgnutls26, libgpgme6, libgs8, libgsasl7, libgsmme1c2a, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtk-vnc-1.0-0, libgtk2-perl, libgtk2.0-cil, libgwenhywfar47, libgwrapguile1, libhal-storage1, libhal1, libhesiod0, libhsqldb-java, libhtml-format-perl, libhtml-template-perl, libhttp-recorder-perl, libhttp-request-params-perl, libhunspell-1.2-0, libhyphen0, libical0, libicu36, libid3-3.8.3, libident, libiec61883-0, libilmbase6, libio-compress-base-perl, libio-compress-zlib-perl, libio-socket-inet6-perl, libio-string-perl, libio-zlib-perl, libiptcdata0, libiso9660-3, libiso9660-dev, libjack0, libjasper1, libjaxp1.2-java, libjaxp1.3-java, libjline-java, libkdeedu3, libkeyutils1, libkiten1, libktoblzcheck1c2a, liblapack3gf, liblazy1, libldap-2.4-2, liblockdev1, liblog4j1.2-java, libloudmouth1-0, liblua5.1-0, liblua50, liblualib50, liblzo2-2, libmail-sendmail-perl, libmail-spf-perl, libmail-spf-query-perl, libmalaga7, libmcrypt4, libmcs1, libmd5-perl, libmdbtools, libmhash2, libmikmod2, libmime-types-perl, libmodplug0c2, libmoe1.5, libmono-cairo1.0-cil, libmono-corlib1.0-cil, libmono-i18n1.0-cil, libmono-system1.0-cil, libmowgli1, libmozjs0d, libmpcdec3, libmtp7, libmx4j-java, libmyspell3c2, libncursesw5, libneon25, libneon26, libnet-cidr-lite-perl, libnet-daemon-perl, libnet-dbus-perl, libnet-dns-perl, libnet-ip-perl, libnet-ph-perl, libnet-snpp-perl, libnet-ssleay-perl, libnet-telnet-perl, libnetaddr-ip-perl, libnettle2, libnewt0.52, libnl1-pre6, libnotify1, libnspr4-0d, libnss3-0d, libntlm0, libobjc1, libobject-realize-later-perl, libobparser21, liboil0.3, libonig2, libopenal0a, libopenal1, libopenexr6, libopensync0, libpaper-utils, libparse-recdescent-perl, libpcap0.8, libpci3, libpixman-1-0, libpkcs11-helper1, libplot2c2, libplrpc-perl, libpoppler-glib3, libpoppler3, libportaudio0, libpq4, libqt3-mt, libraw1394-8, libregexp-java, librplay3, libruby1.6, libsablot0, libsasl2-2, libsasl2-modules, libsepol1, libserf-0-0, libservlet2.3-java, libservlet2.4-java, libsieve2-1, libsilc-1.1-2, libslang2, libsmpeg0, libsocket6-perl, libsoup2.4-1, libspectre1, libsplashy1, libsqlite3-0, libssh2-1, libssl0.9.8, libstdc++6, libsuitesparse-3.1.0, libswfdec-0.6-90, libsys-hostname-long-perl, libsysfs2, libtalloc1, libtasn1-3, libtelepathy-glib0, libtelepathy2, libthai-data, libthai0, libtie-ixhash-perl, libtrackerclient0, libts-0.0-0, libttf2, libufsparse, libuser-identity-perl, libuuid-perl, libvoikko1, libvte9, libwpd8c2a, libwpg-0.1-1, libwps-0.1-1, libx11-data, libxapian15, libxau6, libxcb-render-util0, libxcb-render0, libxcb-xlib0, libxcb1, libxcomposite1, libxdamage1, libxdmcp6, libxfce4util4, libxfcegui4-4, libxfixes3, libxfont1, libxinerama1, libxkbfile1, libxklavier12, libxml-handler-trees-perl, libxml-parser-perl, libxml-perl, libxml-regexp-perl, libxml-twig-perl, libxml-xpath-perl, libxprintapputil1, libxprintutil1, libxss1, libxt-java, libxul-common, libxul0d, libxxf86dga1, libxxf86misc1, libxxf86vm1, libzvt2.0-0, libzzip-0-12, linux-libc-dev, lp-solve, lpr, lsb-base, lsb-release, lwm, lxsession-lite, lxterminal, lynx-cur, lzma, make, mono-common, mono-jit, mozilla-thunderbird, mpc, ncurses-term, netcat-openbsd, netrik, nginx, nullmailer, ocaml-findlib, ocrad, openssl, oroborus, oss-compat, pcscd, pm-utils, postgresql-client-7.4, postgresql-client-common, preview-latex-style, procmail, pwm, python2.3-cjkcodecs, python2.3-iconvcodec, python2.3-japanese-codecs, python2.3-korean-codecs, python2.5, python2.5-minimal, ratpoison, rdesktop, readline-common, refblas3, rkhunter, rlpr, rox-filer, roxterm, runit, sapphire, sodipodi, ssl-cert, stalonetray, swfdec-gnome, swfdec-mozilla, sysvinit-utils, tcl8.0, tcl8.5, telepathy-gabble, terminal, thy, timezoneconf, tinywm, tk8.5, tsclient, ttf-dustin, ttf-freefont, ttf-kochi-gothic, ttf-liberation, ttf-sjfonts, twm, tzdata, ucspi-unix, unace, unhide, unzoo, virtualbox-ose-guest-utils, vtwm, w3c-dtd-xhtml, w9wm, wdg-html-reference, windowlab, wm2, wmii2, x11-apps, x11-common, x11-session-utils, x11-xfs-utils, x11-xkb-utils, x11-xserver-utils, x11proto-core-dev, x11proto-print-dev, xauth, xbitmaps, xcursor-themes, xfonts-encodings, xfonts-utils, xinit, xkb-data-legacy, xprint-utils, xterm, xutils-dev, yaird] # starts : 282 # conflicts : 550062 # decisions : 1157536 # propagations : 88799950 # inspects : 428208745 # shortcuts : 0 # learnt literals : 46 # learnt binary clauses : 85 # learnt ternary clauses : 46 # learnt constraints : 550016 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 2108891 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 28 # Number of update (reduction) of LBD : 10851 # 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) : 311566.74654662446 # non guided choices 170745 # learnt constraints type # org.sat4j.minisat.constraints.cnf.LearntBinaryClause => 85 # org.sat4j.minisat.constraints.cnf.LearntWLClause => 62809 # Solving done (289.828s). # WARNING: The solution found MIGHT NOT BE optimal # Solution contains:876