# Checking available version of Java # Java(TM) SE Runtime Environment (build 1.6.0_22-b04) # Running really p2cudf # Solver launched on Thu Aug 25 16:11:38 CEST 2011 # Using input file /home/misc2010/data/2011/incremental/s-e-l-s-s/rand519.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand519.cudf.s-e-l-s-s.result # Objective function -removed,-changed # Timeout 280s # java.runtime.name Java(TM) SE Runtime Environment # java.vm.name Java HotSpot(TM) Server VM # java.vm.version 17.1-b03 # java.vm.vendor Sun Microsystems Inc. # sun.arch.data.model 32 # java.version 1.6.0_22 # os.name Linux # os.version 2.6.18-6-xen-amd64 # os.arch i386 # Free memory 705643136 # Max memory 709558272 # Total memory 709558272 # Number of processors 1 # Parsing ... # Time to parse:3042 # Parsing done (3.045s). # Solving ... # Request size: 992 # Number of packages after slice: 8286 # Slice efficiency: 90% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@148cc8c # 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 learned constraints deletion strategy # timeout=280s # DB Simplification allowed=false # --- End Solver configuration --- # Optimization function: User defined:-removed,-changed # criteria removed size is 950 using new vars 9237 to 10187 # criteria changed size is 3311 using new vars 10187 to 13498 # p cnf 13497 84100 # Current objective function value: 403(0.722s) # Current objective function value: 402(1.242s) # Current objective function value: 227(1.729s) # Current objective function value: 226(2.209s) # Current objective function value: 138(2.654s) # Current objective function value: 137(3.149s) # Current objective function value: 132(3.352s) # Current objective function value: 119(3.565s) # Current objective function value: 112(3.826s) # Current objective function value: 78(3.958s) # Current objective function value: 77(4.124s) # Current objective function value: 70(4.213s) # Current objective function value: 69(4.263s) # Current objective function value: 66(4.328s) # Current objective function value: 64(4.357s) # Current objective function value: 63(4.411s) # Current objective function value: 62(4.511s) # Current objective function value: 61(4.548s) # Found optimal criterion number 1 # Current objective function value: 800(4.596s) # cleaning 2429 clauses out of 4858 with flag 5000/8015 # cleaning 4189 clauses out of 8387 with flag 11000/14015 # cleaning 5587 clauses out of 11184 with flag 18000/21015 # cleaning 6727 clauses out of 13516 with flag 26000/29015 # Current objective function value: 799(31.964s) # cleaning 6076 clauses out of 12159 with flag 1000/34398 # cleaning 6034 clauses out of 12087 with flag 7005/40403 # cleaning 6517 clauses out of 13052 with flag 14004/47402 # cleaning 7251 clauses out of 14530 with flag 22002/55400 # cleaning 8130 clauses out of 16275 with flag 31001/64399 # Current objective function value: 798(82.888s) # Current objective function value: 788(83.058s) # cleaning 11138 clauses out of 22275 with flag 5000/78538 # cleaning 8564 clauses out of 17138 with flag 11001/84539 # cleaning 7776 clauses out of 15574 with flag 18001/91539 # cleaning 7899 clauses out of 15798 with flag 26001/99539 # cleaning 8448 clauses out of 16898 with flag 35000/108538 # cleaning 9220 clauses out of 18450 with flag 45000/118538 # cleaning 10105 clauses out of 20230 with flag 56000/129538 # cleaning 11058 clauses out of 22126 with flag 68001/141539 # cleaning 12026 clauses out of 24067 with flag 81000/154538 # cleaning 13020 clauses out of 26039 with flag 95000/168538 # cleaning 13997 clauses out of 28019 with flag 110000/183538 # cleaning 14992 clauses out of 30021 with flag 126000/199538 # cleaning 16010 clauses out of 32033 with flag 143004/216542 # cleaning 17010 clauses out of 34020 with flag 161001/234539 # cleaning 18004 clauses out of 36008 with flag 180000/253538 # cleaning 18990 clauses out of 38003 with flag 200000/273538 # cleaning 20003 clauses out of 40013 with flag 221000/294538 # Solver timed out after 280.092s) # -removed criteria value: 61 # Removed packages: [abiword-gnome, akode, aptitude, capplets, cpio, gnome, gnome-applets, gnome-core, gnome-desktop-environment, gnome-office, ipchains, kappfinder, kcmlinuz, kde, kde-amusements, kde-core, kde-devel, kde-devel-extras, kdebase, kdebase-dev, kdegames, kdelibs4, kdelibs4-dev, kdemultimedia, kdemultimedia-kappfinder-data, kdesdk, kdevelop3-data, kdevelop3-plugins, kmessedwords, kpoker, kspy, libarts1, libarts1-dev, libdps1, libgtkhtml2-0, libjack0.80.0-0, libjack0.80.0-dev, libkcal2a, libkdeedu1, libkdenetwork2, libkdepim1, libkleopatra0a, libkonq4-dev, libmagick6, libmimelib1a, libmodplug0, libnautilus2-2, libperl5.8, libqt3-mt-dev, libqt3c102-mt, libxft1, libxklavier8, linux-kernel-headers, nautilus-media, secpolicy, tasksel, vimpart, xfree86-common, xlibmesa-glu-dev, xlibs, xserver-common] # -changed criteria value: 788 # Changed packages: [abiword-common, abiword-gnome, akode, akregator, amor, apt, apt-utils, aptitude, ark, arts, artsbuilder, atlantik, atlantikdesigner, binutils, blinken, ca-certificates, capplets, capplets-data, cdrdao, cdrecord, cervisia, coreutils, cpio, cyrus-admin-2.2, dbus, dbus-x11, dcoprss, debian-archive-keyring, debian-el, doc-debian, doc-linux-ja-html, dpkg, dpkg-dev-el, dvd+rw-tools, eject, emacs21, emacs21-bin-common, emacs21-common, emacsen-common, eyesapplet, fenix-plugin-mpeg, fifteenapplet, flow-tools, fontconfig, fontconfig-config, gcc-4.4-base, gconf2, gconf2-common, genisoimage, gnome, gnome-about, gnome-applets, gnome-cards-data, gnome-control-center, gnome-core, gnome-desktop-data, gnome-desktop-environment, gnome-doc-utils, gnome-games, gnome-games-data, gnome-icon-theme, gnome-menus, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnumeric, gnumeric-common, icedove, icedove-locale-pt-br, imagemagick, indi, ipchains, juk, kaboodle, kaddressbook, kaddressbook-plugins, kalarm, kalzium, kalzium-data, kamera, kanagram, kandy, kappfinder, karm, kasteroids, kate, kate-plugins, katomic, kaudiocreator, kbabel, kbackgammon, kbattleship, kblackbox, kbounce, kbruch, kbugbuster, kcachegrind, kcalc, kcharselect, kcmlinuz, kcoloredit, kcontrol, kcron, kdat, kdbg, kde, kde-amusements, kde-core, kde-devel, kde-devel-extras, kdeaddons, kdeaddons-kfile-plugins, kdeadmin, kdeadmin-kfile-plugins, kdeartwork-style, kdeartwork-theme-window, kdebase, kdebase-bin, kdebase-bin-kde3, kdebase-data, kdebase-dev, kdebase-kio-plugins, kdeedu, kdeedu-data, kdeeject, kdegames, kdegraphics-kfile-plugins, kdelibs, kdelibs-bin, kdelibs-data, kdelibs4, kdelibs4-dev, kdelibs4c2a, kdelirc, kdemultimedia, kdemultimedia-kappfinder-data, kdemultimedia-kfile-plugins, kdemultimedia-kio-plugins, kdenetwork, kdenetwork-filesharing, kdenetwork-kfile-plugins, kdepasswd, kdepim, kdepim-kfile-plugins, kdepim-kio-plugins, kdepim-kresources, kdepim-wizards, kdeprint, kdesdk, kdesdk-kfile-plugins, kdesdk-misc, kdesktop, kdessh, kdevelop, kdevelop-data, kdevelop3, kdevelop3-data, kdevelop3-plugins, kdf, kdict, kdnssd, kdvi, kedit, keduca, kenolaba, kfax, kfilereplace, kfind, kfloppy, kfouleggs, kgamma, kget, kghostview, kgoldrunner, kgpg, khangman, khelpcenter, khexedit, kicker, kicker-applets, kiconedit, kig, kimagemapeditor, kitchensync, kiten, kjots, kjumpingcube, klaptopdaemon, klatin, kleopatra, klettres, klettres-data, klickety, klines, klinkstatus, klipper, kmahjongg, kmail, kmailcvt, kmenuedit, kmessedwords, kmid, kmilo, kmines, kmix, kmoon, kmplot, kmrml, kmtrace, knetworkconf, knewsticker, knewsticker-scripts, knode, knotes, kodo, kolf, kolourpaint, kommander, kompare, konq-plugins, konqueror, konqueror-nsplugins, konquest, konsole, konsolekalendar, kontact, kooka, kopete, korganizer, korn, kpackage, kpager, kpat, kpdf, kpercentage, kpersonalizer, kpf, kpilot, kpoker, kpovmodeler, kppp, kprof, krdc, krec, kregexpeditor, kreversi, krfb, kruler, ksame, kscd, kscreensaver, kscreensaver-xsavers, kshisen, ksig, ksim, ksirc, ksirtet, ksmiletris, ksmserver, ksnake, ksnapshot, ksokoban, kspaceduel, ksplash, kspy, kstars, kstars-data, ksvg, ksync, ksysguard, ksysguardd, ksysv, kteatime, ktimer, ktip, ktnef, ktouch, ktron, ktuberling, kturtle, ktux, kuickshow, kuiviewer, kuser, kverbos, kview, kviewshell, kvoctrain, kwalletmanager, kweather, kwifimanager, kwin, kwin4, kwordquiz, kworldclock, kxsldbg, liba52-0.7.4, libakode2, libart-2.0-2, libart-2.0-dev, libarts1, libarts1-audiofile, libarts1-dev, libarts1-mpeglib, libarts1-xine, libarts1c2a, libartsc0, libartsc0-dev, libasound2, libasound2-dev, libatk1.0-0, libatk1.0-dev, libattr1, libavahi-client-dev, libavahi-client3, libavahi-common-data, libavahi-common-dev, libavahi-common3, libavahi-compat-libdnssd1, libavahi-glib-dev, libavahi-glib1, libavahi-qt3-1, libavcodec0d, libb-hooks-endofscope-perl, libb-hooks-op-check-perl, libbluetooth2, libbonobo2-0, libbonobo2-common, libbonobo2-dev, libbonoboui2-0, libbonoboui2-common, libbonoboui2-dev, libboost-python1.33.1, libc-bin, libc-dev-bin, libc6, libc6-dev, libcairo2, libcairo2-dev, libcamel1.2-8, libclucene0ldbl, libcroco3, libcroco3-dev, libcrypt-dh-perl, libcups2, libcurl3-gnutls, libcvsservice0, libcyrus-imap-perl22, libdata-optlist-perl, libdatrie1, libdb4.3, libdb4.3++c2, libdb4.4, libdb4.7, libdb4.8, libdbus-1-3, libdbus-1-dev, libdbus-glib-1-2, libdbus-qt-1-1c2, libdevel-declare-perl, libdirectfb-1.0-0, libdps1, libdrm2, libebook1.2-5, libecal1.2-6, libedataserver1.2-7, libedataserverui1.2-6, libedit2, libeel2-2.14, libexif12, libexiv2-9, libflac7, libflac8, libfontconfig1, libfontconfig1-dev, libfontenc-dev, libfontenc1, libfreetype6, libfreetype6-dev, libfribidi0, libfs6, libgadu3, libgcc1, libgconf2-4, libgconf2-dev, libgcrypt11, libgcrypt11-dev, libgl1-mesa-dev, libgl1-mesa-dri, libgl1-mesa-glx, libglade2-0, libglade2-dev, libglib2.0-0, libglib2.0-dev, libglu1-mesa, libglu1-mesa-dev, libgmp3c2, libgnokii3, libgnome-desktop-2, libgnome-keyring-dev, libgnome-keyring0, libgnome-menu2, libgnome-window-settings1, libgnome2-0, libgnome2-common, libgnome2-dev, libgnomecanvas2-0, libgnomecanvas2-common, libgnomecanvas2-dev, libgnomecups1.0-1, libgnomeprint2.2-0, libgnomeprint2.2-data, libgnomeprintui2.2-0, libgnomeprintui2.2-common, libgnomeui-0, libgnomeui-common, libgnomeui-dev, libgnomevfs2-0, libgnomevfs2-common, libgnomevfs2-dev, libgnutls13, libgnutls26, libgoffice-0.8-8, libgoffice-0.8-8-common, libgpg-error-dev, libgpg-error0, libgphoto2-2, libgphoto2-port0, libgsf-1-114, libgsf-1-common, libgsmme1c2a, libgssapi-krb5-2, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtk2.0-0, libgtk2.0-dev, libgtkhtml2-0, libhal-storage1, libhal1, libhtml-parser-perl, libice-dev, libice6, libidl-dev, libidl0, libidn11, libidn11-dev, libilmbase6, libindex0, libiodbc2, libiw29, libjack0, libjack0.80.0-0, libjack0.80.0-dev, libjasper1, libk5crypto3, libkcal2a, libkcal2b, libkcddb1, libkdecore5, libkdeedu1, libkdeedu3, libkdegames1, libkdenetwork2, libkdepim1, libkdepim1a, libkdeui5, libkeyutils1, libkgantt0, libkio5, libkiten1, libkjsapi4, libkjsembed4, libkleopatra0a, libkleopatra1, libkmime2, libkonq4, libkonq4-dev, libkparts4, libkpimexchange1, libkpimidentities1, libkrb5-3, libkrb53, libkrb5support0, libkrosscore4, libkscan1, libksieve0, libktnef1, libldap-2.4-2, liblocale-gettext-perl, liblockdev1, libltdl7, liblua50, liblualib50, liblzma2, libmad0, libmad0-dev, libmagick6, libmagick9, libmeanwhile1, libmemcache0, libmetacity0, libmimelib1a, libmimelib1c2a, libmng-dev, libmng1, libmodplug0, libmodplug0c2, libmozjs0d, libmysqlclient12, libnautilus-burn3, libnautilus-extension1, libnautilus2-2, libncurses5, libncurses5-dev, libncursesw5, libnspr4-0d, libnss3-0d, libogg-dev, libogg0, libopencdk8, libopencdk8-dev, libopenexr6, liborbit2, liborbit2-dev, libpam0g, libpanel-applet2-0, libpanel-applet2-dev, libpango1.0-0, libpango1.0-common, libpango1.0-dev, libparams-util-perl, libpcre3, libpcre3-dev, libpcrecpp0, libperl5.10, libperl5.8, libpisock9, libpixman-1-0, libpixman-1-dev, libpng12-0, libpng12-dev, libpoppler-qt2, libpoppler3, libpopt-dev, libpopt0, libpostproc0d, libpq3, libpthread-stubs0, libpthread-stubs0-dev, libqt3-mt, libqt3-mt-dev, libqt3c102-mt, libqt4-dbus, libqt4-network, libqt4-script, libqt4-svg, libqt4-xml, libqtcore4, libqtgui4, libraptor1, librasqal2, libraw1394-8, librdf0, libreadline5, libreadline6, librss1, librsvg2-2, librsvg2-common, librsvg2-dev, libsasl2-2, libsasl2-modules, libsdl-mixer1.2, libsdl1.2debian, libsdl1.2debian-oss, libselinux1, libselinux1-dev, libsensors3, libsepol1, libsepol1-dev, libsm-dev, libsm6, libsmbclient, libsmpeg0, libsnmp-base, libsnmp15, libsolid4, libsoprano4, libspeex1, libsqlite3-0, libssl0.9.8, libstdc++6, libstreamanalyzer0, libstreams0, libsub-exporter-perl, libsub-install-perl, libsub-name-perl, libsysfs2, libtag1-vanilla, libtag1c2a, libtasn1-3, libterm-readkey-perl, libterm-readline-perl-perl, libtext-charwidth-perl, libtext-iconv-perl, libthai-data, libthai0, libtotem-plparser1, libts-0.0-0, libusb-0.1-4, libvariable-magic-perl, libvorbis-dev, libvorbis0a, libvorbisenc2, libvorbisfile3, libvte9, libwnck18, libx11-6, libx11-data, libx11-dev, libxau-dev, libxau6, libxaw7, libxcb-render-util0, libxcb-render-util0-dev, libxcb-render0, libxcb-render0-dev, libxcb1, libxcb1-dev, libxcomposite-dev, libxcomposite1, libxdamage-dev, libxdamage1, libxdmcp-dev, libxdmcp6, libxext-dev, libxext6, libxfixes-dev, libxfixes3, libxfont-dev, libxfont1, libxft-dev, libxft1, libxft2, libxi-dev, libxi6, libxine1, libxinerama-dev, libxinerama1, libxkbfile1, libxklavier10, libxklavier8, libxml2, libxml2-dev, libxmu-dev, libxmu-headers, libxmu6, libxmuu1, libxp6, libxpm4, libxrandr-dev, libxrandr2, libxres1, libxslt1.1, libxss1, libxt-dev, libxt6, libxtrap6, libxtst6, libxul-common, libxul0d, libxv-dev, libxv1, libxvmc1, libxxf86dga1, libxxf86misc1, libxxf86vm1, lighttpd, lighttpd-mod-trigger-b4-dl, linux-kernel-headers, linux-libc-dev, lsb-base, lskat, man-db, mesa-common-dev, metacity-common, mkisofs, mpeglib, mysql-common-4.1, nautilus, nautilus-cd-burner, nautilus-data, nautilus-media, ncurses-bin, networkstatus, noatun, noatun-plugins, openssh-blacklist, openssh-client, openssh-server, openssl, oss-compat, perl, perl-base, perl-modules, perl-suid, pinentry-qt, poxml, python, python-gmenu, python-minimal, python-support, python2.3-libxml2, python2.4, python2.6, python2.6-minimal, qt3-designer, qt3-dev-tools, quanta, quanta-data, readline-common, reportbug, secpolicy, soprano-daemon, ssh, synaptic, tasksel, thunderbird-locale-pt-br, tk8.4, tk8.4-dev, totem, totem-xine, ttf-dustin, ttf-kochi-mincho, ttf-sjfonts, umbrello, vimpart, wireless-tools, wodim, x-dev, x11-common, x11-xserver-utils, x11proto-composite-dev, x11proto-core-dev, x11proto-damage-dev, x11proto-fixes-dev, x11proto-fonts-dev, x11proto-input-dev, x11proto-kb-dev, x11proto-randr-dev, x11proto-video-dev, x11proto-xext-dev, x11proto-xinerama-dev, xauth, xaw3dg, xbase-clients, xbitmaps, xcursor-themes, xfonts-100dpi, xfonts-75dpi, xfonts-base, xfonts-encodings, xfonts-scalable, xfonts-utils, xfree86-common, xkb-data, xlibmesa-dri, xlibmesa-gl, xlibmesa-gl-dev, xlibmesa-glu, xlibmesa-glu-dev, xlibs, xlibs-data, xlibs-static-dev, xserver-common, xserver-xfree86, xserver-xorg, xserver-xorg-core, xserver-xorg-input-ur98, xserver-xorg-video-vmware, xtrans-dev, xutils, xutils-dev, xz-lzma, xz-utils, yelp, zlib1g, zlib1g-dev] # starts : 195 # conflicts : 302183 # decisions : 2211040 # propagations : 492450477 # inspects : 1275085449 # shortcuts : 0 # learnt literals : 397 # learnt binary clauses : 2171 # learnt ternary clauses : 860 # learnt constraints : 301785 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 1081242 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 26 # 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) : 2498797.295445896 # non guided choices 523155 # learnt constraints type # org.sat4j.minisat.constraints.cnf.LearntBinaryClause => 964 # org.sat4j.minisat.constraints.cnf.LearntWLClause => 26691 # Solving done (282.731s). # WARNING: The solution found MIGHT NOT BE optimal # Solution contains:1194