# Solver launched on Mon Sep 03 02:51:38 UTC 2012 # Using input file /home/competition/data/upgrade/easy/rand213.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/dist-upgrade/upgrade/easy/rand213.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:6850 # Parsing done (6.855s). # Solving ... # Request size: 1012 # Number of packages after slice: 8039 # Slice efficiency: 85% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@7e0c2ff5 # 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 11219 to 11219 # criteria aligned(source,sourceversion) size is 5772 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 5772 using new vars 11219 to 14113 # criteria new size is 2907 using new vars 14113 to 17020 # p cnf 17019 86784 # Found optimal criterion number 1 # Current objective function value: 6(1.925s) # Current objective function value: 5(2.221s) # Current objective function value: 4(2.436s) # Current objective function value: 2(2.591s) # cleaning 2541 clauses out of 5094 with flag 10887/5115 # cleaning 4277 clauses out of 8553 with flag 23931/11115 # cleaning 5633 clauses out of 11276 with flag 39319/18115 # cleaning 6817 clauses out of 13644 with flag 59042/26116 # cleaning 7907 clauses out of 15827 with flag 79917/35116 # cleaning 8953 clauses out of 17919 with flag 101161/45115 # cleaning 9976 clauses out of 19966 with flag 124953/56115 # cleaning 10995 clauses out of 21990 with flag 152925/68115 # cleaning 11992 clauses out of 23995 with flag 188984/81115 # cleaning 12997 clauses out of 26004 with flag 229261/95116 # cleaning 13992 clauses out of 28006 with flag 271962/110115 # cleaning 15003 clauses out of 30015 with flag 319340/126116 # cleaning 15999 clauses out of 32012 with flag 367017/143116 # cleaning 17000 clauses out of 34012 with flag 415073/161115 # cleaning 18006 clauses out of 36012 with flag 470154/180115 # cleaning 19001 clauses out of 38006 with flag 525595/200115 # cleaning 20001 clauses out of 40006 with flag 584843/221116 # cleaning 20996 clauses out of 42004 with flag 643788/243115 # cleaning 21998 clauses out of 44009 with flag 701892/266116 # cleaning 23002 clauses out of 46011 with flag 760665/290116 # cleaning 23994 clauses out of 48008 with flag 827719/315115 # cleaning 24998 clauses out of 50014 with flag 896363/341115 # cleaning 26000 clauses out of 52016 with flag 970832/368115 # cleaning 27008 clauses out of 54016 with flag 1045041/396115 # cleaning 27996 clauses out of 56009 with flag 1118146/425116 # cleaning 29002 clauses out of 58013 with flag 1194074/455116 # cleaning 29990 clauses out of 60011 with flag 1273953/486116 # cleaning 31002 clauses out of 62020 with flag 1353488/518115 # cleaning 32010 clauses out of 64019 with flag 1434878/551116 # Solver timed out after 285.197s) # -new criteria value: 504 # Newly installed packages: [9base, 9menu, a2ps, aewm, aewm++, af, akregator, altgcc, antlr, app-install-data, aspell-en, aspell-es, aspell-ukr, busybox, ca-certificates, cdcd, cdebconf, cdrdao, chimera2, clamav-data, classpath-tools, cli-common, console-terminus, cpp-4.1, cramfsprogs, cronosii, dash, dbus, dbus-x11, debconf-english, debian-archive-keyring, devfsd, discover1-data, dmz-cursor-theme, dvi2tty, dviutils, egroupware-egw-pear, epdfview, epos-ktd, epos-lpc, epos-ptd, fastjar, festival, festlex-cmu, festlex-poslex, festvox-kallpc16k, festvox-kdlpc16k, festvox-suopuhe-common, festvox-suopuhe-mv, fontconfig-config, fvwm-icons, gamin, gawk, gcc-4.1-base, gcc-4.3-base, gconf2-common, gdk-imlib11, ghostscript, ghostscript-x, gij-3.3, gnome-audio, gnome-backgrounds, gnome-bin, gnome-doc-utils, gnome-games-extra-data, gnome-libs-data, gnustep-back, gnustep-base-common, gnustep-common, gnustep-gui-common, gnustep-ppd, gpgv, grep-dctrl, gtk2-engines, guile-1.6, hal-info, hardinfo, herrie, hoichess, host, hunspell-ar, hunspell-en-us, hunspell-se, hunspell-uz, industrial-cursor-theme, iportuguese, ispell, jwm, krb4-config, kterm, lacheck, ladcca2, lapack3, larswm, latex-xcolor, ldso, libacr38u, libalut0, libao2, libapr1, libaprutil1, libarchive1, libart2, libasyncns0, libavahi-client3, libavahi-common-data, libavahi-common3, libavahi-glib1, libbcel-java, libbeecrypt6, libbinio1ldbl, libblas3gf, libcairo-perl, libcairo2, libcairomm-1.0-1, libcamel1.2-11, libcanna1g, libcap2, libccid, libcdaudio1, libcddb2, libcitadel1, libclass-accessor-perl, libclucene0ldbl, libcolorblind0, libcompress-zlib-perl, libcteco50000, libcups2, libcupsimage2, libcupsys2, libcurl3-gnutls, libcxxtools6, libdatrie0, libdb2, libdb4.4, libdb4.5, libdb4.6, libdbi-perl, libdbus-1-3, libdbus-glib-1-2, libdc1394-13, libdebian-installer4, libdevel-symdump-perl, libdigest-hmac-perl, libdigest-sha1-perl, libdirectfb-1.0-0, libdirectfb-extra, libdmx1, libdrm2, libeb12, libedataserver1.2-9, libedit2, libelfg0, libept0, liberror-perl, libestools1.2, libetoken, libetpan13, libevtlog0, libexempi3, libfaad0, libffcall1, libffi5, libfile-ncopy-perl, libfile-remove-perl, libflac8, libfont-afm-perl, libfontenc1, libforms1, libfreezethaw-perl, libfs6, libfsplib0, libg2c0, libgalago3, libgamin0, libgcj-common, libgcj4, libgcr410, libgd2-xpm, libgdk-pixbuf2, libgdome2-0, libgdome2-cpp-smart0c2a, libgecko2.0-cil, libgfortran3, libggz2, libgif4, libgl1-mesa-glide3, libglew1, libglib-perl, libglib2.0-cil, libglide3, libglu1-mesa, libgmime2.1, libgmp3, libgnome2-vfs-perl, libgnome32, libgnomekbd-common, libgnomeprint-bin, libgnomeprint-data, libgnomeprint15, libgnomesupport0, libgnomeui32, libgnorba27, libgnorbagtk0, 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, libguppi16, libgwenhywfar47, libgwrapguile1, libhal-storage1, libhal1, libhesiod0, libhtml-format-perl, libhtml-template-perl, libhunspell-1.2-0, libhyphen0, libibverbs1, libical0, libicu36, libid3-3.8.3, libident, libiec61883-0, libio-compress-base-perl, libio-socket-inet6-perl, libio-string-perl, libio-zlib-perl, libiptcdata0, libjaxp1.2-java, libjaxp1.3-java, libkeyutils1, libktoblzcheck1c2a, liblapack3gf, liblazy1, libldap-2.4-2, liblog4j1.2-java, libloudmouth1-0, liblua5.1-0, liblzo2-2, libmail-sendmail-perl, libmail-spf-query-perl, libmalaga7, libmcrypt4, libmcs1, libmdbtools, libmhash2, libmikmod2, libmodplug0c2, libmoe1.5, libmono-cairo1.0-cil, libmono-corlib1.0-cil, libmono-system1.0-cil, libmowgli1, libmozjs0d, libmpcdec3, libmtp7, libmusicbrainz4c2a, libmx4j-java, libncursesw5, libneon25, libneon26, libnet-cidr-lite-perl, libnet-daemon-perl, libnet-dns-perl, libnet-ip-perl, libnet-ph-perl, libnet-snpp-perl, libnet-ssleay-perl, libnet-telnet-perl, libnettle2, libnewt0.52, libnl1-pre6, libnspr4-0d, libnss3-0d, libnss3-1d, libntlm0, libobjc1, libobject-realize-later-perl, liboil0.3, libonig2, libopenal0, libopenal1, libopensync0, liborbit0, libparse-recdescent-perl, libpcap0.8, libpci3, libpixman-1-0, libpkcs11-helper1, libplot2c2, libplrpc-perl, libpoppler-glib3, libpoppler3, libpopplerkit0, libportaudio0, libpq4, libraw1394-8, librdmacm-dev, librdmacm1, libregexp-java, librplay3, libruby1.6, libsablot0c102, libsasl2-2, libsasl2-modules, libserf-0-0, libservlet2.3-java, libservlet2.4-java, libsieve2-1, libsilc-1.1-2, libslang2, libslbreflex2, libsmpeg0, libsndfile1, libsocket6-perl, libsoup2.4-1, libspectre1, libspiff1, 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, libtotem-plparser10, libtrackerclient0, libts-0.0-0, libttf2, libufsparse, liburiparser1, libuser-identity-perl, libversion-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, libxml1, libxprintapputil1, libxprintutil1, libxss1, libxt-java, libxul-common, libxul0d, libxxf86dga1, libxxf86misc1, libxxf86vm1, libzvt2.0-0, libzzip-0-12, lp-solve, lprng, lsb-base, lsb-release, lwm, lxsession-lite, lxterminal, lynx-cur, lzma, make, mono-common, mono-jit, mozilla-thunderbird, myspell-fa, myspell-hr, myspell-hy, myspell-ku, myspell-pt-br, myspell-sk, ncurses-term, netcat-openbsd, netrik, nginx, nullmailer, ocrad, openbox, openssl, openssl-blacklist, openvpn-blacklist, oroborus, pcscd, perl-doc, php-pear, php5-cli, php5-common, pm-utils, postgresql-client-7.4, postgresql-client-common, preview-latex-style, pterm, pwm, python-cups, python-fpconst, python-gdata, python-gobject, python-libxml2, python-minimal, python-support, python2.5, python2.5-minimal, qca-tls, qvwm, ratpoison, rdesktop, readline-common, refblas3, rlpr, rox-filer, roxterm, rsyslog, sapphire, sg3-utils, sodipodi, ssl-cert, stalonetray, swfdec-gnome, swfdec-mozilla, tcl8.0, tcl8.5, telepathy-gabble, terminal, thy, timezoneconf, tinywm, tk8.5, tsclient, ttf-freefont, ttf-liberation, twm, tzdata, ucspi-unix, unzoo, virtualbox-ose-guest-utils, vtwm, w3c-dtd-xhtml, w9wm, wdg-html-reference, wgerman-medical, windowlab, wm2, wmii2, x11-apps, x11-common, x11-session-utils, x11-utils, x11-xfs-utils, x11-xkb-utils, x11-xserver-utils, x11proto-core-dev, x11proto-print-dev, xauth, xbitmaps, xcursor-themes, xfonts-encodings, xfonts-konsole, xfonts-utils, xinit, xkb-data-legacy, xprint-utils, xsltproc, xterm, xutils-dev, yaird] # starts : 297 # conflicts : 570037 # decisions : 1166203 # propagations : 94403214 # inspects : 393582153 # shortcuts : 0 # learnt literals : 21 # learnt binary clauses : 67 # learnt ternary clauses : 29 # learnt constraints : 570016 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 2122455 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 29 # Number of update (reduction) of LBD : 13486 # 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) : 331228.8875088155 # non guided choices 95812 # learnt constraints type # org.sat4j.minisat.constraints.cnf.LearntBinaryClause => 67 # org.sat4j.minisat.constraints.cnf.LearntWLClause => 50863 # Solving done (291.943s). # WARNING: The solution found MIGHT NOT BE optimal # Solution contains:810