HEAD is now at 2b6ae8b initial deployement # 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 15:27:48 CEST 2011 # Using input file /home/misc2010/data/2011/incremental/s-e-l-s-s/rand314.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand314.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:3110 # Parsing done (3.112s). # Solving ... # Request size: 992 # Number of packages after slice: 8389 # 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 9340 to 10290 # criteria changed size is 3355 using new vars 10290 to 13645 # p cnf 13644 85592 # Current objective function value: 474(0.735s) # Current objective function value: 471(0.98s) # Current objective function value: 470(1.248s) # Current objective function value: 465(1.597s) # Current objective function value: 103(1.953s) # Current objective function value: 64(2.035s) # Current objective function value: 63(2.212s) # Current objective function value: 62(2.342s) # Current objective function value: 61(2.451s) # Current objective function value: 60(3.035s) # Current objective function value: 59(3.295s) # Current objective function value: 58(3.494s) # Current objective function value: 57(3.727s) # Found optimal criterion number 1 # Current objective function value: 529(3.802s) # Current objective function value: 434(5.349s) # Current objective function value: 402(5.576s) # Current objective function value: 401(6.373s) # Current objective function value: 393(6.623s) # Current objective function value: 391(7.886s) # cleaning 3355 clauses out of 6718 with flag 3001/8796 # cleaning 4680 clauses out of 9359 with flag 9000/14795 # Current objective function value: 390(19.059s) # Current objective function value: 387(19.11s) # cleaning 5008 clauses out of 10032 with flag 5002/20149 # cleaning 5508 clauses out of 11020 with flag 11000/26147 # cleaning 6256 clauses out of 12511 with flag 18002/33149 # cleaning 7121 clauses out of 14251 with flag 26001/41148 # cleaning 8063 clauses out of 16128 with flag 35000/50147 # cleaning 9025 clauses out of 18064 with flag 45000/60147 # Current objective function value: 386(88.258s) # cleaning 7303 clauses out of 14622 with flag 2016/65730 # cleaning 6650 clauses out of 13302 with flag 8000/71714 # cleaning 6821 clauses out of 13653 with flag 15001/78715 # cleaning 7406 clauses out of 14831 with flag 23000/86714 # cleaning 8179 clauses out of 16425 with flag 32000/95714 # cleaning 9110 clauses out of 18249 with flag 42003/105717 # cleaning 10069 clauses out of 20137 with flag 53001/116715 # cleaning 11022 clauses out of 22063 with flag 65000/128714 # cleaning 12020 clauses out of 24039 with flag 78001/141715 # cleaning 13005 clauses out of 26018 with flag 92000/155714 # cleaning 13998 clauses out of 28013 with flag 107000/170714 # Current objective function value: 385(271.957s) # cleaning 15902 clauses out of 31817 with flag 5000/188516 # Solver timed out after 280.09s) # -removed criteria value: 57 # Removed packages: [aptitude, capplets, dirmngr, gnome, gnome-desktop-environment, gtk2-engines-spherecrystal, gucharmap, kde, kde-devel, kde-devel-extras, kdebase-dev, kdelibs4-dev, kdenetwork, kdepim, kdesdk, kleopatra, kpf, kspy, ksync, libarts1-dev, libbonoboui2-dev, libcupsys2-dev, libdps1, libgcrypt11-dev, libglade2-dev, libgnome2-dev, libgnomecanvas2-dev, libgnomeui-dev, libgnomevfs2-dev, libgnutls11-dev, libgpg-error-dev, libgtk2.0-dev, libgtkgl2.0-dev, libgtkspell-dev, libkonq4-dev, liblablgtk2-ocaml-dev, libmagick6, libmodplug0, libnautilus2-2, libopencdk8-dev, libpanel-applet2-dev, libpango1.0-dev, libqt3-mt-dev, librsvg2-dev, libxft-dev, libxft1, libxklavier8, linux-kernel-headers, nautilus-media, pppoeconf, tasksel, whiptail, xfree86-common, xlibmesa-glu-dev, xlibs, xlibs-static-dev, xserver-common] # -changed criteria value: 385 # Changed packages: [apache, apache-common, apache2-utils, apt, apt-utils, aptitude, binutils, blacs1gf-mpich, capplets, capplets-data, cdrdao, cdrecord, coreutils, crossfire-client, crossfire-client-x11, debian-archive-keyring, dialog, dirmngr, dpkg, dvd+rw-tools, egroupware-core, egroupware-developer-tools, fontconfig, fontconfig-config, gcc-4.4-base, gconf2, gconf2-common, genisoimage, gnome, gnome-about, gnome-applets, gnome-applets-data, gnome-cards-data, gnome-control-center, gnome-desktop-data, gnome-desktop-environment, gnome-games, gnome-games-data, gnome-icon-theme, gnome-menus, gnome-panel, gnome-panel-data, gnome-session, gnome-themes-extras, gnumeric, gnumeric-common, gnuplot, gnuplot-nox, gnuplot-x11, gstreamer0.10-alsa, gtk2-engines, gtk2-engines-crux, gtk2-engines-industrial, gtk2-engines-lighthouseblue, gtk2-engines-mist, gtk2-engines-redmond95, gtk2-engines-spherecrystal, gtk2-engines-thinice, gucharmap, imagemagick, industrial-cursor-theme, kde, kde-devel, kde-devel-extras, kdebase-dev, kdelibs4-dev, kdenetwork, kdepim, kdesdk, kleopatra, kpf, kspy, ksync, liba52-0.7.4, libapache-mod-php4, libarts1-dev, libasound2, libasound2-dev, libatk1.0-0, libatk1.0-dev, libatlas3gf-sse3, libavahi-client3, libavahi-common-data, libavahi-common3, libavahi-glib1, libavcodec0d, libbonobo2-0, libbonobo2-common, libbonobo2-dev, libbonoboui2-dev, libc-bin, libc-dev-bin, libc6, libc6-dev, libcairo2, libcamel1.2-8, libcroco3, libcroco3-dev, libcups2, libcupsys2, libcupsys2-dev, libdatrie1, libdb4.4, libdb4.8, libdbus-1-3, libdbus-glib-1-2, libdps1, libdrm2, libebook1.2-5, libecal1.2-6, libedataserver1.2-7, libedataserverui1.2-6, libeel2-2.14, libexif12, libfontconfig1, libfontconfig1-dev, libfontenc1, libfreetype6, libfreetype6-dev, libfs6, libgcc1, libgconf2-4, libgconf2-dev, libgcrypt11, libgcrypt11-dev, libgd2-xpm, libgfortran3, libgl1-mesa-dev, libgl1-mesa-dri, libgl1-mesa-glx, libglade2-0, libglade2-dev, libglib2.0-0, libglib2.0-dev, libglu1-mesa, libglu1-mesa-dev, 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, libgnupg-perl, libgnutls11-dev, libgnutls13, libgnutls26, libgoffice-1-2, libgoffice-1-common, libgpg-error-dev, libgpg-error0, libgsf-1-114, libgsf-1-common, libgsf-gnome-1-114, libgssapi-krb5-2, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtk2.0-0, libgtk2.0-dev, libgtkgl2.0-dev, libgtkspell-dev, libgtop2-7, libgtop2-common, libhal-storage1, libhal1, libice-dev, libice6, libidl-dev, libidl0, libjasper1, libk5crypto3, libkeyutils1, libkonq4-dev, libkrb5-3, libkrb53, libkrb5support0, liblablgtk2-ocaml-dev, liblua5.1-0, liblwp-protocol-http-socketunix-perl, libmagick++9c2a, libmagick6, libmagick9, libmetacity0, libmodplug0, libmodplug0c2, libmpich1.0gf, libmysqlclient15off, libnasl2, libnautilus-burn3, libnautilus-extension1, libnautilus2-2, libncurses5, libncurses5-dev, libncursesw5, libnessus2, libnotify1, libnspr4-0d, libnss3-0d, libogg-dev, libogg0, libopencdk8, libopencdk8-dev, liborbit2, liborbit2-dev, libpanel-applet2-0, libpanel-applet2-dev, libpango1.0-0, libpango1.0-common, libpango1.0-dev, libpcre3, libpcre3-dev, libpcrecpp0, libpixman-1-0, libplot2c2, libpng12-0, libpng12-dev, libpopt-dev, libpopt0, libpostproc0d, libpstoedit0c2a, libqt3-mt-dev, libreadline5, libreadline6, librsvg2-2, librsvg2-common, librsvg2-dev, libselinux1, libsm-dev, libsm6, libspeex1, libsqlite3-0, libssl0.9.8, libstdc++6, libtasn1-3, libthai-data, libthai0, libtotem-plparser1, libvorbis-dev, libvorbis0a, libvorbisenc2, libvorbisfile3, libvte9, libwnck18, libx11-6, libx11-data, libx11-dev, libxau-dev, libxau6, libxaw7, libxcb-render-util0, libxcb-render0, libxcb1, libxcomposite1, libxdamage1, libxdmcp-dev, libxdmcp6, libxext-dev, libxext6, libxfixes3, libxfont1, libxft-dev, libxft1, libxi-dev, libxi6, libxine1, libxinerama1, libxkbfile1, libxklavier10, libxklavier8, libxml-parser-perl, libxml-xpath-perl, libxml2, libxml2-dev, libxmu-dev, libxmu-headers, libxmu6, libxmuu1, libxp6, libxpm4, libxrandr-dev, libxrandr2, libxres1, libxslt1.1, libxss1, libxt-dev, libxt6, libxtrap6, libxtst6, libxv-dev, libxv1, libxvmc1, libxxf86dga1, libxxf86misc1, libxxf86vm1, libzzip-0-12, linux-kernel-headers, linux-libc-dev, lsb-base, lzma, mesa-common-dev, metacity-common, mkisofs, mpich-bin, mysql-common, nautilus, nautilus-cd-burner, nautilus-data, nautilus-media, ncurses-bin, php-fpdf, php4-cli, php4-common, php4-gd, php4-mysql, pppoeconf, python, python-central, python-gmenu, python-gnuplot, python-minimal, python-numpy, python-support, python2.6, python2.6-minimal, readline-common, scalapack-mpich-test, scalapack-test-common, scalapack1-mpich, synaptic, tasksel, totem, totem-xine, virtualbox-ose-guest-utils, whiptail, wodim, x-dev, x11-common, x11-xkb-utils, x11proto-core-dev, x11proto-input-dev, x11proto-kb-dev, x11proto-randr-dev, x11proto-video-dev, x11proto-xext-dev, xbase-clients, xbitmaps, xcursor-themes, xfonts-100dpi, xfonts-75dpi, xfonts-base, xfonts-encodings, xfonts-scalable, xfonts-utils, xfree86-common, xkb-data-legacy, 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, xtrans-dev, xutils, xutils-dev] # starts : 146 # conflicts : 188582 # decisions : 1565273 # propagations : 524873613 # inspects : 1484940329 # shortcuts : 0 # learnt literals : 246 # learnt binary clauses : 1650 # learnt ternary clauses : 736 # learnt constraints : 188335 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 526826 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 20 # 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) : 6.4212578052361146E7 # non guided choices 445364 # learnt constraints type # org.sat4j.minisat.constraints.cnf.LearntBinaryClause => 864 # org.sat4j.minisat.constraints.cnf.LearntWLClause => 15117 # Solving done (282.72s). # WARNING: The solution found MIGHT NOT BE optimal # Solution contains:1072