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 16:29:27 CEST 2011 # Using input file /home/misc2010/data/2011/incremental/s-e-l-s/rand439.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand439.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:3069 # Parsing done (3.072s). # Solving ... # Request size: 992 # Number of packages after slice: 7668 # Slice efficiency: 91% # --- 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 8619 to 9569 # criteria changed size is 3172 using new vars 9569 to 12741 # p cnf 12740 78040 # Current objective function value: 533(0.526s) # Current objective function value: 532(0.71s) # Current objective function value: 396(0.833s) # Current objective function value: 356(0.953s) # Current objective function value: 355(1.261s) # Current objective function value: 84(1.327s) # Current objective function value: 83(1.371s) # Current objective function value: 77(1.421s) # Found optimal criterion number 1 # Current objective function value: 221(1.48s) # Current objective function value: 220(2.061s) # Current objective function value: 216(2.148s) # Current objective function value: 215(2.217s) # Found optimal solution for the last criterion # -removed criteria value: 77 # Removed packages: [adduser, base-config, capplets, cron, dbus-1, dbus-glib-1, debconf-i18n, dirmngr, exim4, exim4-base, exim4-config, exim4-daemon-light, gdm, gimp, gksu, gnome, gnome-applets, gnome-control-center, gnome-core, gnome-desktop-environment, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnome-terminal, gnome-themes, gnome-volume-manager, gtk2-engines-mist, hal, kamera, kde, kde-amusements, kde-core, kde-devel, kde-devel-extras, kdebase, kdebase-dev, kdegraphics, kdelibs4-dev, kdepim, kdesdk, kdessh, kdeutils, kedit, kleopatra, kooka, ksplash, kspy, libarts1-dev, libdps1, libgimpprint1, libgphoto2-2, libhal-storage0, libhal0, libkonq4-dev, libkscan1, libmagick6, libnautilus-burn0, libpng12-dev, libpt-plugins-oss, libqt3-mt-dev, libsane, libtext-iconv-perl, libxft1, libxmu-dev, modutils, nautilus, nautilus-cd-burner, nautilus-media, sane-utils, ssh, totem, totem-xine, xfree86-common, xlibmesa-glu-dev, xlibs, xserver-common] # -changed criteria value: 215 # Changed packages: [adduser, anacron, base-config, capplets, cron, dbus-1, dbus-glib-1, debconf-english, debconf-i18n, dirmngr, exim4, exim4-base, exim4-config, exim4-daemon-light, fontconfig, fontconfig-config, gcc-4.4-base, gdm, gimp, git, gksu, gnome, gnome-applets, gnome-control-center, gnome-core, gnome-desktop-environment, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnome-terminal, gnome-themes, gnome-volume-manager, gs-common, gs-gpl, gtk2-engines-mist, hal, imagemagick, kamera, kde, kde-amusements, kde-core, kde-devel, kde-devel-extras, kdebase, kdebase-dev, kdegraphics, kdelibs4-dev, kdepim, kdesdk, kdessh, kdeutils, kedit, kleopatra, kooka, ksplash, kspy, libarts1-dev, libc6, libc6-dev, libclass-accessor-perl, libdbus-1-3, libdbus-1-dev, libdps1, libdrm2, libebml-dev, libfontconfig1, libfontconfig1-dev, libfontenc-dev, libfontenc1, libfreetype6, libfreetype6-dev, libfs6, libgbf-1-common, libgcc1, libgcrypt11, libgcrypt11-dev, libgimpprint1, libgl1-mesa-dev, libgl1-mesa-dri, libgl1-mesa-glx, libglu1-mesa, libglu1-mesa-dev, libgnutls13, libgpg-error-dev, libgpg-error0, libgphoto2-2, libgphoto2-port0, libgsasl7, libhal-dev, libhal-storage0, libhal-storage1, libhal0, libhal1, libhd13, libhd13-dev, libice-dev, libice6, libidn11, libidn11-dev, libio-string-perl, libiw28, libkonq4-dev, libkrb53, libkscan1, libmagick6, libmagick9, libmatroska-dev, libnautilus-burn0, libopencdk8, libopencdk8-dev, libparse-debianchangelog-perl, libpng12-0, libpng12-dev, libpt-1.10.10-plugins-oss, libpt-plugins-oss, libqt3-mt-dev, libsane, libsm-dev, libsm6, libstdc++6, libsysfs2, libtasn1-3, libtext-iconv-perl, libusb-0.1-4, libx11-6, libx11-data, libx11-dev, libxau-dev, libxau6, libxaw7, libxdmcp-dev, libxdmcp6, libxext-dev, libxext6, libxfont-dev, libxfont1, libxft-dev, libxft1, libxft2, libxi-dev, libxi6, libxkbfile1, libxml2, libxml2-dev, libxmu-dev, libxmu6, libxmuu1, libxp6, libxpm4, libxrandr-dev, libxrandr2, libxslt1.1, libxss1, libxt-dev, libxt6, libxtrap6, libxtst6, libxv-dev, libxv1, libxxf86dga1, libxxf86vm1, lsb-base, mesa-common-dev, module-init-tools, modutils, mpop, nautilus, nautilus-cd-burner, nautilus-media, pmount, sane-utils, ssh, totem, totem-xine, tzdata, x-dev, x11-common, x11proto-core-dev, x11proto-fonts-dev, x11proto-input-dev, x11proto-kb-dev, x11proto-randr-dev, x11proto-scrnsaver-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, xmail, xserver-common, xserver-xfree86, xserver-xorg, xserver-xorg-core, xserver-xorg-input-void, xserver-xorg-video-voodoo, xtrans-dev, xutils, xutils-dev] # starts : 15 # conflicts : 2722 # decisions : 237984 # propagations : 4217289 # inspects : 15540587 # shortcuts : 0 # learnt literals : 138 # learnt binary clauses : 427 # learnt ternary clauses : 214 # learnt constraints : 2582 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 2169 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 0 # 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) : 2727871.28072445 # non guided choices 118413 # learnt constraints type # Solving done (6.282s). # The solution found IS optimal # Solution contains:945