# Solver launched on Mon Sep 03 03:10:43 UTC 2012 # Using input file /home/competition/data/upgrade/easy/rand653.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/dist-upgrade/upgrade/easy/rand653.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:5444 # Parsing done (5.451s). # Solving ... # Request size: 1012 # Number of packages after slice: 8082 # 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 11276 to 11276 # criteria aligned(source,sourceversion) size is 5818 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 5818 using new vars 11276 to 14187 # criteria new size is 2922 using new vars 14187 to 17109 # p cnf 17108 87130 # Found optimal criterion number 1 # Current objective function value: 7(1.83s) # Current objective function value: 5(2.11s) # Current objective function value: 2(2.388s) # cleaning 2603 clauses out of 5216 with flag 12344/5228 # cleaning 4298 clauses out of 8613 with flag 24767/11228 # cleaning 5652 clauses out of 11316 with flag 39150/18229 # cleaning 6826 clauses out of 13663 with flag 55645/26228 # cleaning 7911 clauses out of 15837 with flag 74011/35228 # cleaning 8964 clauses out of 17927 with flag 94563/45229 # cleaning 9981 clauses out of 19962 with flag 117326/56228 # cleaning 10982 clauses out of 21982 with flag 143228/68229 # cleaning 11987 clauses out of 23999 with flag 169919/81228 # cleaning 13004 clauses out of 26012 with flag 198444/95228 # cleaning 13996 clauses out of 28008 with flag 231265/110228 # cleaning 15001 clauses out of 30012 with flag 264374/126228 # cleaning 16001 clauses out of 32011 with flag 299313/143228 # cleaning 16997 clauses out of 34010 with flag 336553/161228 # cleaning 17997 clauses out of 36013 with flag 375544/180228 # cleaning 19008 clauses out of 38016 with flag 416329/200228 # cleaning 20004 clauses out of 40009 with flag 459194/221229 # cleaning 20997 clauses out of 42004 with flag 504452/243228 # cleaning 21995 clauses out of 44008 with flag 552136/266229 # cleaning 22999 clauses out of 46013 with flag 601861/290229 # cleaning 24007 clauses out of 48013 with flag 653194/315228 # cleaning 24995 clauses out of 50007 with flag 706356/341229 # cleaning 26000 clauses out of 52013 with flag 761408/368230 # cleaning 26998 clauses out of 54012 with flag 819301/396229 # cleaning 27999 clauses out of 56013 with flag 877704/425228 # cleaning 29003 clauses out of 58014 with flag 937979/455228 # Solver timed out after 285.171s) # -new criteria value: 489 # Newly installed packages: [9base, 9menu, a2ps, aewm, aewm++, af, akregator, anacron, apache2-common, apache2-mpm-prefork, apache2-utils, app-install-data, aspell-es, aspell-ukr, bincimap, bincimap-run, blt, bogofilter-common, busybox, ca-certificates, cdcd, cdrdao, checkpw, chimera2, clamav-data, classpath-tools, cli-common, console-terminus, cpp-4.3, cramfsprogs, dash, dbus, debconf-english, debian-archive-keyring, devfsd, dialog, discover1-data, dmz-cursor-theme, dvi2tty, dviutils, epdfview, epos-ktd, epos-lpc, epos-ptd, esound-clients, expect, fastjar, festival, festlex-cmu, festlex-poslex, festvox-kallpc16k, festvox-kdlpc16k, festvox-suopuhe-common, festvox-suopuhe-mv, fontconfig-config, gawk, gcc-4.3-base, gconf2-common, gdk-imlib11, ghostscript, ghostscript-x, gij-3.3, gnome-audio, gnome-backgrounds, gnome-bin, gnome-games-extra-data, gnome-libs-data, gpgv, grep-dctrl, guile-1.6, hal-info, hardinfo, host, icedove, icedove-l10n-it, icedove-locale-it, industrial-cursor-theme, iproute, ipsvd, jed-common, jikes, jwm, kazehakase, kbd, krb4-config, ktalkd, kterm, lacheck, lapack3, larswm, latex-xcolor, ldso, lesstif2, libacr38u, libalut0, libao2, libapache2-mod-php4, libapr1, libaprutil1, libarchive1, libart2, libasyncns0, libatm1, libavahi-client3, libavahi-common-data, libavahi-common3, libavahi-glib1, libbcel-java, libbeecrypt6, libbinio1ldbl, libblas3gf, libcairo2, libcairomm-1.0-1, libcamel1.2-11, libcanna1g, libcap2, libccid, libcdaudio1, libcddb2, libcitadel1, libclass-accessor-perl, libclucene0ldbl, libcolorblind0, libcompress-zlib-perl, libconvert-asn1-perl, libcrypt-smbhash-perl, libcteco50000, libcups2, libcupsimage2, libcxxtools6, libdatrie0, libdb2, libdb4.4, libdb4.5, libdb4.6, libdbus-1-3, libdbus-glib-1-2, libdc1394-13, libdebian-installer4, libdevel-symdump-perl, libdigest-hmac-perl, libdigest-md4-perl, libdigest-sha1-perl, libdirectfb-1.0-0, libdirectfb-extra, libdmx1, libdrm2, libeb12, libedataserver1.2-9, libedit2, libelfg0, libept0, liberror-perl, libestools1.2, libetoken, libevtlog0, libexempi3, libfaad0, libffi5, libfile-ncopy-perl, libfile-remove-perl, libfont-afm-perl, libfontenc1, libforms1, libfreezethaw-perl, libfs6, libfsplib0, libg2c0, libgalago3, 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, libgmp3c2, libgnome2-vfs-perl, libgnome32, libgnomekbd-common, libgnomeprint-bin, libgnomeprint-data, libgnomeprint15, libgnomesupport0, libgnomeui32, libgnorba27, libgnorbagtk0, libgnutls26, libgomp1, 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, 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, libjcode-pm-perl, libkeyutils1, libktoblzcheck1c2a, liblapack3gf, liblazy1, libldap-2.4-2, liblockdev1, liblog4j1.2-java, libloudmouth1-0, liblua5.1-0, liblzo2-2, libmagick9, libmail-sendmail-perl, libmail-spf-query-perl, libmalaga7, libmatrixssl1.8, libmcrypt4, libmcs1, libmdbtools, libmhash2, libmikmod2, libmoe1.5, libmono-cairo1.0-cil, libmono-corlib1.0-cil, libmono-system1.0-cil, libmowgli1, libmozjs0d, libmpcdec3, libmpfr1ldbl, libmtp7, libmx4j-java, libmyspell3c2, libncursesw5, libneon26, libnet-cidr-lite-perl, libnet-daemon-perl, libnet-dns-perl, libnet-ip-perl, libnet-ldap-perl, libnet-perl, libnet-ph-perl, libnet-snpp-perl, libnet-ssleay-perl, libnet-telnet-perl, libnettle2, libnl1, libnotify1, libnspr4-0d, libnss3-0d, libnss3-1d, libntlm0, libobject-realize-later-perl, liboil0.3, libonig2, libopenal0, libopenal1, libopensync0, liborbit0, libparse-recdescent-perl, libpcap0.8, libpixman-1-0, libpkcs11-helper1, libplot2c2, libplrpc-perl, libpoppler-glib3, libpoppler3, libpopplerkit0, libportaudio0, libpq3, libpq4, libpth20, libraw1394-8, libregexp-java, librep9, libruby1.6, libsablot0, libsasl2-2, libsasl2-modules, 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, libtotem-plparser10, libtrackerclient0, libts-0.0-0, libttf2, libufsparse, libunicode-map8-perl, libunicode-string-perl, 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-regexp-perl, libxml1, libxprintapputil1, libxprintutil1, libxss1, libxt-java, libxul-common, libxul0d, libxxf86dga1, libxxf86misc1, libxxf86vm1, libzvt2.0-0, libzzip-0-12, lilo-config, links, lisa, locales, lp-solve, lpr, lsb-base, lsb-release, lwm, lxsession-lite, lxterminal, lynx-cur, make, mono-common, mono-jit, mozilla-thunderbird, mozilla-thunderbird-locale-it, ncurses-term, netcat-openbsd, netrik, nginx, ocrad, openssl, openssl-blacklist, openvpn-blacklist, oroborus, pcscd, perl-doc, php4-common, php4-pgsql, pm-utils, preview-latex-style, pterm, pwm, python-fpconst, python-support, python2.3-cjkcodecs, python2.3-iconvcodec, python2.3-japanese-codecs, python2.3-korean-codecs, python2.4, python2.4-logilab-common, python2.4-pylint, python2.4-tk, qvwm, ratpoison, rdesktop, readline-common, refblas3, rlinetd, rlpr, rox-filer, roxterm, rsyslog, runit, samba, samba-common, samba-dbg, sapphire, sodipodi, ssl-cert, ssmtp, stalonetray, swfdec-gnome, swfdec-mozilla, tcl8.0, tcl8.5, telepathy-gabble, thy, timezoneconf, tinywm, tk8.5, trayer, tsclient, ttf-liberation, twm, tzdata, ucspi-unix, unace, unzoo, vim-lesstif, virtualbox-ose-guest-utils, w3c-dtd-xhtml, w9wm, wdg-html-reference, windowlab, wm2, wmii, 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-utils, xinit, xkb-data-legacy, xprint-utils, xterm, xutils-dev, yaird, ytalk] # starts : 258 # conflicts : 485065 # decisions : 1062265 # propagations : 75089559 # inspects : 371408193 # shortcuts : 0 # learnt literals : 12 # learnt binary clauses : 116 # learnt ternary clauses : 49 # learnt constraints : 485053 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 2850097 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 26 # Number of update (reduction) of LBD : 8082 # 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) : 263461.9681345632 # non guided choices 169720 # learnt constraints type # org.sat4j.minisat.constraints.cnf.LearntBinaryClause => 116 # org.sat4j.minisat.constraints.cnf.LearntWLClause => 58732 # Solving done (290.762s). # WARNING: The solution found MIGHT NOT BE optimal # Solution contains:1059