# Solver launched on Mon Sep 03 03:10:27 UTC 2012 # Using input file /home/competition/data/upgrade/easy/rand813.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/dist-upgrade/upgrade/easy/rand813.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:5488 # Parsing done (5.494s). # Solving ... # Request size: 1012 # Number of packages after slice: 8168 # 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 11422 to 11422 # criteria aligned(source,sourceversion) size is 5804 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 5804 using new vars 11422 to 14330 # criteria new size is 2968 using new vars 14330 to 17298 # p cnf 17297 87867 # Found optimal criterion number 1 # Current objective function value: 6(1.03s) # Current objective function value: 11(1.258s) # Current objective function value: 7(1.417s) # cleaning 2586 clauses out of 5176 with flag 10704/5187 # cleaning 4291 clauses out of 8590 with flag 23753/11187 # cleaning 5649 clauses out of 11298 with flag 38199/18186 # cleaning 6821 clauses out of 13650 with flag 54815/26187 # cleaning 7911 clauses out of 15829 with flag 73363/35187 # cleaning 8955 clauses out of 17918 with flag 94040/45187 # cleaning 9981 clauses out of 19962 with flag 118476/56186 # cleaning 10978 clauses out of 21982 with flag 148220/68187 # cleaning 11996 clauses out of 24003 with flag 182148/81186 # cleaning 12999 clauses out of 26007 with flag 218596/95186 # cleaning 13991 clauses out of 28008 with flag 254967/110186 # cleaning 15002 clauses out of 30019 with flag 295440/126188 # cleaning 16008 clauses out of 32015 with flag 335782/143186 # cleaning 16996 clauses out of 34007 with flag 375400/161186 # cleaning 17994 clauses out of 36011 with flag 416254/180186 # cleaning 18997 clauses out of 38018 with flag 457867/200187 # cleaning 20009 clauses out of 40021 with flag 501265/221187 # cleaning 21001 clauses out of 42012 with flag 547397/243187 # Current objective function value: 6(164.645s) # cleaning 13302 clauses out of 26616 with flag 2118/248792 # cleaning 9651 clauses out of 19313 with flag 14240/254791 # cleaning 8328 clauses out of 16663 with flag 28327/261792 # cleaning 8159 clauses out of 16335 with flag 44384/269792 # cleaning 8584 clauses out of 17175 with flag 63881/278791 # cleaning 9288 clauses out of 18592 with flag 84111/288792 # cleaning 10149 clauses out of 20304 with flag 106622/299792 # cleaning 11068 clauses out of 22154 with flag 132251/311791 # cleaning 12042 clauses out of 24086 with flag 162049/324791 # cleaning 13015 clauses out of 26044 with flag 195228/338791 # cleaning 14008 clauses out of 28029 with flag 234222/353791 # cleaning 15011 clauses out of 30022 with flag 275835/369792 # cleaning 15998 clauses out of 32011 with flag 317357/386792 # cleaning 16998 clauses out of 34013 with flag 360195/404792 # cleaning 18004 clauses out of 36015 with flag 403536/423792 # cleaning 18994 clauses out of 38010 with flag 450545/443791 # cleaning 20009 clauses out of 40017 with flag 499928/464792 # cleaning 20997 clauses out of 42008 with flag 551875/486792 # cleaning 22001 clauses out of 44011 with flag 604501/509792 # Solver timed out after 285.376s) # -new criteria value: 598 # Newly installed packages: [9menu, a2ps, aewm, af, altgcc, amaya, app-install-data, aspell, aspell-bin, aspell-es, aspell-ukr, blam, bluez-gnome, busybox, ca-certificates, cdcd, cdrdao, chimera2, clamav-data, classpath-tools, cli-common, console-terminus, cpp-4.1, cramfsprogs, cronosii, dash, dbus, dbus-x11, dctrl-tools, debconf-english, debian-archive-keyring, devfsd, discover1-data, dmz-cursor-theme, dvi2tty, dviutils, egroupware-egw-pear, enlightenment-data, epdfview, epos-ktd, epos-lpc, epos-ptd, esound-clients, fastjar, festival, festlex-cmu, festlex-poslex, festvox-kallpc16k, festvox-kdlpc16k, festvox-suopuhe-common, festvox-suopuhe-mv, fontconfig-config, freetds-common, ftdi-eeprom, gamin, gawk, gcc-3.4-base, gcc-4.1-base, gcc-4.3-base, gcompris-data, gcompris-sound-eu, gconf2-common, gdk-imlib1, gdk-imlib11, ghostscript, ghostscript-x, gij-3.3, gnome-audio, gnome-bin, gnome-games-extra-data, gnome-libs-data, gnome-media-common, gnome-netstatus-applet, gnome-spell, gnuchess, gnuchess-book, gnustep-back-common, gnustep-base-common, gnustep-common, gnustep-gui-common, gnustep-ppd, gpgv, gtk2-engines, guile-1.6, hal-info, hardinfo, host, html2text, industrial-cursor-theme, ion2, jwm, kdelibs4c2a, krb4-config, kterm, lapack3, larswm, latex-beamer, latex-xcolor, ldso, lesstif2, libacr38u, libalut0, libao2, libapr1, libaprutil1, libarchive1, libart2, libart2.0-cil, libarts1c2a, libasedrive-usb, libasyncns0, libatlas3gf-3dnow, libavahi-client3, libavahi-common-data, libavahi-common3, libavahi-glib1, libavahi-qt3-1, libbcel-java, libbeecrypt6, libbinio1ldbl, libblas3gf, libcairo-perl, libcairo2, libcairomm-1.0-1, libcamel1.2-11, libcanna1g, libcap2, libcdaudio1, libcddb2, libcitadel1, libclass-accessor-perl, libclucene0ldbl, libcolorblind0, libcompress-raw-zlib-perl, libcompress-zlib-perl, libconfuse0, libcteco50000, libcups2, libcupsimage2, libcupsys2, libcxxtools3, libdate-manip-perl, libdatrie0, libdb2, libdb4.4, libdb4.5, libdb4.6, libdbd-mysql-perl, libdbi-perl, libdbus-1-3, libdbus-glib-1-2, libdbus-qt-1-1c2, libdebian-installer4, libdevel-symdump-perl, libdigest-hmac-perl, libdigest-sha1-perl, libdirectfb-1.0-0, libdirectfb-extra, libdmx1, libdrm2, libeb12, libedataserver1.2-9, libedit2, libefs1, libelfg0, libept0, liberror-perl, libestools1.2, libevtlog0, libexempi3, libexif12, libfaad0, libffcall1, libffi5, libfile-ncopy-perl, libfile-remove-perl, libflite1, libfont-afm-perl, libfontenc1, libforms1, libfreezethaw-perl, libfs6, libfsplib0, libftdi1, libg2c0, libgalago3, libgamin0, libgcj-common, libgcj4, libgconf2.0-cil, libgcr410, libgd2-xpm, libgdiplus, libgdk-pixbuf2, libgdome2-0, libgdome2-cpp-smart0c2a, libgecko2.0-cil, libgempc410, libgfortran3, libggz2, libgif4, libgl1-mesa-glide3, libglade2.0-cil, libglew1, libglib-perl, libglib2.0-cil, libglib2.0-data, libglide3, libglu1-mesa, libgmime2.1, libgmp3, libgnome-vfs2.0-cil, libgnome2-vfs-perl, libgnome2.0-cil, libgnome32, libgnomekbd-common, libgnomeprint-bin, libgnomeprint-data, libgnomeprint15, libgnomesupport0, libgnomeui32, libgnorba27, libgnorbagtk0, libgnustep-base1.10, libgnutls13, libgnutls26, libgpgme6, libgs8, libgsasl7, libgsmme1c2a, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtk-vnc-1.0-0, libgtk2-perl, libgtk2.0-cil, libgtksourceview2.0-0, libgtksourceview2.0-cil, libgtksourceview2.0-common, 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, libio-compress-base-perl, libio-compress-zlib-perl, libio-socket-inet6-perl, libio-socket-ssl-perl, libio-string-perl, libio-zlib-perl, libiptcdata0, libjack0.100.0-0, libjaxp1.2-java, libjaxp1.3-java, libjline-java, libkeyutils1, libkleopatra1, libkpathsea4, libktoblzcheck1c2a, liblapack3gf, liblazy1, libldap-2.4-2, liblog4j1.2-java, libloudmouth1-0, libltdl3, liblua5.1-0, liblua50, liblualib50, liblzo2-2, libmail-sendmail-perl, libmail-spf-perl, libmail-spf-query-perl, libmalaga7, libmcrypt4, libmcs1, libmdbtools, libmeanwhile1, libmhash2, libmikmod2, libmodplug0c2, libmoe1.5, libmono-accessibility2.0-cil, libmono-addins-gui0.2-cil, libmono-addins0.2-cil, libmono-cairo1.0-cil, libmono-cairo2.0-cil, libmono-corlib1.0-cil, libmono-corlib2.0-cil, libmono-data-tds1.0-cil, libmono-data-tds2.0-cil, libmono-i18n1.0-cil, libmono-i18n2.0-cil, libmono-mozilla0.2-cil, libmono-security1.0-cil, libmono-security2.0-cil, libmono-sharpzip0.84-cil, libmono-sharpzip2.84-cil, libmono-sqlite2.0-cil, libmono-system-data1.0-cil, libmono-system-data2.0-cil, libmono-system-runtime2.0-cil, libmono-system-web1.0-cil, libmono-system-web2.0-cil, libmono-system1.0-cil, libmono-system2.0-cil, libmono-winforms2.0-cil, libmono0, libmono1.0-cil, libmono2.0-cil, libmowgli1, libmozjs0d, libmpcdec3, libmusicbrainz4c2a, libmx4j-java, libmyspell3c2, libmysqlclient10, libmysqlclient12, libmysqlclient15off, libnautilus-extension1, libncursesw5, libndesk-dbus-glib1.0-cil, libndesk-dbus1.0-cil, libneedle-ruby1.8, libneon25, libneon26, libnet-cidr-lite-perl, libnet-daemon-perl, libnet-dbus-perl, libnet-dns-perl, libnet-ip-perl, libnet-ph-perl, libnet-sftp-ruby1.8, libnet-snpp-perl, libnet-ssh-ruby1.8, libnet-ssleay-perl, libnet-telnet-perl, libnetaddr-ip-perl, libnettle2, libnewt0.52, libnl1, libnotify1, libnspr4-0d, libnss3-0d, libnss3-1d, libntlm0, libobjc1, libobject-realize-later-perl, liboil0.3, libonig2, libopenal0, libopenal1, libopenexr2c2a, libopenssl-ruby1.8, libopensync0, liborbit0, libpaper-utils, libparse-recdescent-perl, libpcap0.8, libpci3, libpixman-1-0, libpkcs11-helper1, libplot2, libplrpc-perl, libpng10-0, libpoppler-glib3, libpoppler0c2, libpoppler3, libpopplerkit0, libpq3, libpq4, libpt-plugins-alsa, libpt-plugins-v4l, libpth20, libqt3-mt, libregexp-java, librplay3, libruby1.6, libruby1.8, libsablot0c102, libsane-extras, libsasl2-2, libsasl2-modules, libsdl-mixer1.2, libsdl1.2debian-nas, libserf-0-0, libservlet2.3-java, libservlet2.4-java, libsieve2-1, libsilc-1.1-2, libslang2, libsmpeg0, libsocket6-perl, libsoup2.4-1, libspectre1, libsplashy1, libsqlite0, libsqlite3-0, libssh2-1, libssl0.9.8, libstdc++6, libsuitesparse-3.1.0, libswfdec-0.6-90, libsys-hostname-long-perl, libsysfs2, libtag1c2a, libtalloc1, libtasn1-3, libtelepathy-glib0, libtelepathy2, libthai-data, libthai0, libtie-ixhash-perl, libtotem-plparser10, 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, libxine1-bin, 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, locales-all, lp-solve, lpr, lsb-base, lsb-release, lwm, lxsession-lite, lxterminal, lzma, make, metacity-common, mono-common, mono-gac, mono-jit, mono-runtime, monodoc, monodoc-base, monodoc-browser, monodoc-manual, mozilla-thunderbird, mpc, mutt, mysql-client-5.0, mysql-common, mysql-server-5.0, ncurses-term, netcat-openbsd, netrik, nginx, nullmailer, ocrad, odbcinst1, openbox, openssl, openssl-blacklist, openvpn-blacklist, oroborus, p7zip-full, pcscd, pgf, php-pear, php5, php5-cgi, php5-cli, php5-common, pike7.6-core, pike7.6-image, pike7.6-mysql, pinentry-gtk2, pm-utils, preview-latex-style, procmail, psfontmgr, pterm, pwm, python-cups, python-fpconst, python-gdata, python-gobject, python-minimal, python-support, python2.5, python2.5-minimal, qvwm, ratpoison, rdesktop, readline-common, refblas3, rlinetd, rlpr, rox-filer, roxen4, roxterm, rsync, rsyslog, sapphire, seahorse, sodipodi, ssl-cert, stalonetray, swfdec-gnome, swfdec-mozilla, tcl8.0, tcl8.5, telepathy-gabble, tetex-doc, tetex-extra, tex-common, texlive-common, texlive-lang-dutch, thy, tilda, timezoneconf, tinywm, tk8.5, tsclient, ttf-freefont, ttf-liberation, ttf-tamil-fonts, twm, tzdata, ucspi-unix, unzoo, virtualbox-ose-guest-utils, w3c-dtd-xhtml, w9wm, wamerican, wdg-html-reference, windowlab, wm2, wmii, x11-apps, x11-common, x11-session-utils, x11-utils, x11-xfs-utils, x11-xkb-utils, x11proto-core-dev, x11proto-print-dev, xauth, xbitmaps, xcursor-themes, xfonts-encodings, xfonts-utils, xinit, xkb-data-legacy, xprint-utils, xterm, xutils-dev, zip] # starts : 259 # conflicts : 509792 # decisions : 1122599 # propagations : 69306073 # inspects : 324546298 # shortcuts : 0 # learnt literals : 11 # learnt binary clauses : 145 # learnt ternary clauses : 49 # learnt constraints : 509781 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 5112927 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 37 # Number of update (reduction) of LBD : 10004 # 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) : 242903.91240804284 # non guided choices 181076 # learnt constraints type # org.sat4j.minisat.constraints.cnf.LearntBinaryClause => 145 # org.sat4j.minisat.constraints.cnf.LearntWLClause => 21865 # Solving done (290.397s). # WARNING: The solution found MIGHT NOT BE optimal # Solution contains:887