# 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:09:49 CEST 2011 # Using input file /home/misc2010/data/2011/incremental/s-e-l-s/rand208.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand208.cudf.s-e-l-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:3073 # Parsing done (3.075s). # Solving ... # Request size: 992 # Number of packages after slice: 8222 # 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 9173 to 10123 # criteria changed size is 3413 using new vars 10123 to 13536 # p cnf 13535 82728 # Current objective function value: 473(0.876s) # Current objective function value: 405(1.201s) # Current objective function value: 382(1.405s) # Current objective function value: 333(1.539s) # Current objective function value: 147(1.841s) # Current objective function value: 123(2.136s) # Current objective function value: 122(2.806s) # Current objective function value: 82(2.927s) # Current objective function value: 81(3.386s) # Current objective function value: 73(3.454s) # Current objective function value: 72(3.698s) # Current objective function value: 71(3.859s) # Current objective function value: 60(3.894s) # Current objective function value: 59(3.945s) # Current objective function value: 58(4.028s) # Current objective function value: 57(4.127s) # Current objective function value: 56(4.169s) # Found optimal criterion number 1 # Current objective function value: 456(4.227s) # cleaning 2419 clauses out of 4853 with flag 5001/7486 # cleaning 4183 clauses out of 8366 with flag 11000/13485 # cleaning 5578 clauses out of 11161 with flag 18000/20485 # cleaning 6788 clauses out of 13583 with flag 26001/28486 # cleaning 7890 clauses out of 15793 with flag 35000/37485 # cleaning 8940 clauses out of 17903 with flag 45001/47486 # cleaning 9974 clauses out of 19962 with flag 56002/58487 # cleaning 10985 clauses out of 21984 with flag 68000/70485 # cleaning 11996 clauses out of 23999 with flag 81000/83485 # cleaning 12990 clauses out of 26002 with flag 95000/97485 # cleaning 14002 clauses out of 28012 with flag 110000/112485 # cleaning 15002 clauses out of 30011 with flag 126001/128486 # cleaning 16001 clauses out of 32008 with flag 143000/145485 # cleaning 17002 clauses out of 34006 with flag 161000/163485 # cleaning 17999 clauses out of 36004 with flag 180000/182485 # Solver timed out after 280.119s) # -removed criteria value: 56 # Removed packages: [aptitude, capplets, dnsutils, eyesapplet, gnome, gnome-desktop-environment, gnome-nettool, gnome-volume-manager, hal, kalzium, kde, kde-amusements, kde-devel, kde-devel-extras, kdebase-dev, kdeedu, kdelibs4-dev, kdesdk, kdetoys, khangman, kig, klatin, kmessedwords, kspy, kstars, libart-2.0-dev, libbonoboui2-dev, libboost-python1.32.0, libdps1, libgnome2-dev, libgnomecanvas2-dev, libgnomeui-dev, libgnomevfs2-dev, libkdeedu1, libkonq4-dev, liblablgtk2-ocaml-dev, libmagick6, libmodplug0, libnautilus2-2, libpanel-applet2-dev, libpth2, libxft1, libxklavier8, linux-kernel-headers, manpages, nautilus-media, pinentry-qt, python2.3, python2.3-gtk2, python2.3-numeric, tasksel, usbutils, xfree86-common, xlibmesa-glu-dev, xlibs, xserver-common] # -changed criteria value: 456 # Changed packages: [alsa-base, alsa-utils, apt, apt-utils, aptitude, avelsieve, binutils, ca-certificates, capplets, capplets-data, cdrdao, cdrecord, coreutils, dbus, dbus-1-doc, debconf, debian-archive-keyring, dia-common, dia-gnome, dia-libs, dnsutils, dpkg, dvd+rw-tools, eyesapplet, fontconfig, fontconfig-config, fso-frameworkd, fso-gsm0710muxd, 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-nettool, gnome-panel, gnome-panel-data, gnome-session, gnome-volume-manager, gnumeric, gnumeric-common, gstreamer0.10-alsa, gtk2-engines-pixbuf, hal, imagemagick, kalzium, kde, kde-amusements, kde-devel, kde-devel-extras, kdebase-dev, kdeedu, kdelibs4-dev, kdesdk, kdetoys, khangman, kig, klatin, kmessedwords, kspy, kstars, liba52-0.7.4, libamd2.2.0, libarpack2, libart-2.0-2, libart-2.0-dev, libasound2, libasound2-dev, libatk1.0-0, libatk1.0-dev, libavahi-client3, libavahi-common-data, libavahi-common3, libavahi-glib1, libavcodec0d, libblas3gf, libbonobo2-0, libbonobo2-common, libbonobo2-dev, libbonoboui2-0, libbonoboui2-common, libbonoboui2-dev, libboost-python1.32.0, libc-bin, libc-dev-bin, libc6, libc6-dev, libcairo2, libcairo2-dev, libcamd2.2.0, libcamel1.2-8, libccolamd2.7.1, libcholmod1.7.1, libclass-factory-util-perl, libclass-singleton-perl, libcolamd2.7.1, libcroco3, libcroco3-dev, libcups2, libcurl3-gnutls, libcxsparse2.2.3, libdatetime-locale-perl, libdatetime-perl, libdatetime-timezone-perl, libdatrie0, libdb4.4, libdb4.5, libdb4.6, 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, libffi5, libfftw3-3, libfltk1.1, libfontconfig1, libfontconfig1-dev, libfontenc-dev, libfontenc1, libfreetype6, libfreetype6-dev, libfs6, libftgl2, libg2c0, libgcc1, libgconf2-4, libgconf2-dev, libgcrypt11, libgcrypt11-dev, libgfortran3, libgl1-mesa-dev, libgl1-mesa-dri, libgl1-mesa-glx, libglade2-0, libglade2-dev, libglib2.0-0, libglib2.0-dev, libglpk0, libglu1-mesa, libglu1-mesa-dev, libgmp3c2, 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-6, libgoffice-0-6-common, libgomp1, libgpg-error-dev, libgpg-error0, libgraphicsmagick++3, libgraphicsmagick3, libgsf-1-114, libgsf-1-common, libgsf-gnome-1-114, libgstreamer-plugins-base0.10-0, libgstreamer0.10-0, libgtk2.0-0, libgtk2.0-dev, libgtop2-7, libgtop2-common, libhal-storage1, libhal1, libhdf5-mpich-1.8.4, libibverbs1, libice-dev, libice6, libidl-dev, libidl0, libidn11, libidn11-dev, libjasper1, libkdeedu1, libkeyutils1, libkonq4-dev, libkrb53, liblablgtk2-ocaml-dev, liblapack3gf, liblcms1, liblcms1-dev, libldap-2.4-2, libltdl7, libmagick6, libmagick9, libmetacity0, libmodplug0, libmodplug0c2, libnautilus-burn3, libnautilus-extension1, libnautilus2-2, libncurses5, libncurses5-dev, libncursesw5, libnotify1, libnspr4-0d, libnss3-0d, libogg-dev, libogg0, libopencdk8, libopencdk8-dev, libopenmpi1, liborbit2, liborbit2-dev, libpanel-applet2-0, libpanel-applet2-dev, libpango1.0-0, libpango1.0-common, libpango1.0-dev, libparams-validate-perl, libpcre3, libpcre3-dev, libpcrecpp0, libpixman-1-0, libpixman-1-dev, libpng12-0, libpng12-dev, libpopt-dev, libpopt0, libpostproc0d, libpth2, libpth20, libpthread-stubs0, libpthread-stubs0-dev, libqhull5, libqrupdate1, libreadline5, libreadline6, librose-datetime-perl, librose-object-perl, librsvg2-2, librsvg2-common, librsvg2-dev, libsasl2-2, libselinux1, libsm-dev, libsm6, libspeex1, libsqlite3-0, libssl0.9.8, libstdc++6, libtasn1-3, libthai-data, libthai0, libtotem-plparser1, libumfpack5.4.0, libvorbis-dev, libvorbis0a, libvorbisenc2, libvorbisfile3, libvte9, libwmf0.2-7, 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, libxv-dev, libxv1, libxvmc1, libxxf86dga1, libxxf86misc1, libxxf86vm1, libyaml-0-1, libzzip-0-12, lighttpd, linux-kernel-headers, linux-libc-dev, lsb-base, lsof, lzma, manpages, mesa-common-dev, metacity, metacity-common, mkisofs, modutils, nautilus, nautilus-cd-burner, nautilus-data, nautilus-media, ncurses-bin, netwag, netwox, octave-secs2d, octave3.2, octave3.2-common, openbmap-logger, openssl, php4-cgi, php4-common, pinentry-gtk2, pinentry-qt, planner, procmail, procmail-lib, python, python-cairo, python-central, python-dbus, python-glade2, python-gmenu, python-gobject, python-gst0.10, python-gtk2, python-libxml2, python-minimal, python-numeric, python-serial, python-support, python-yaml, python2.3, python2.3-gtk2, python2.3-numeric, python2.4, python2.5, python2.5-minimal, r-base-core, r-cran-quadprog, readline-common, refblas3, squirrelmail, synaptic, tasksel, totem, totem-xine, usbutils, virtualbox-ose-guest-utils, wodim, x-dev, x11-common, x11-xkb-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, xbase-clients, xbitmaps, xcursor-themes, xdg-utils, 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, xtrans-dev, xutils, xutils-dev, zlib-bin, zlib1g, zlib1g-dev] # starts : 144 # conflicts : 198407 # decisions : 1921152 # propagations : 518269835 # inspects : 1439400196 # shortcuts : 0 # learnt literals : 365 # learnt binary clauses : 2082 # learnt ternary clauses : 737 # learnt constraints : 198041 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 326829 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 15 # 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) : 1878197.5610639995 # non guided choices 557903 # learnt constraints type # org.sat4j.minisat.constraints.cnf.LearntBinaryClause => 1129 # org.sat4j.minisat.constraints.cnf.LearntWLClause => 32798 # Solving done (282.74s). # WARNING: The solution found MIGHT NOT BE optimal # Solution contains:1123