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 18:09:15 CEST 2011 # Using input file /home/misc2010/data/2011/dudf-random/rand992.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand992.cudf.dudf-random.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:2613 # Parsing done (2.616s). # Solving ... # Request size: 2942 # Number of packages after slice: 7694 # Slice efficiency: 87% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@1cdeff # 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 2892 using new vars 10587 to 13479 # criteria changed size is 3962 using new vars 13479 to 17441 # p cnf 17440 79518 # Current objective function value: 523(0.517s) # Current objective function value: 124(0.709s) # Current objective function value: 123(0.96s) # Current objective function value: 122(1.111s) # Current objective function value: 102(1.265s) # Found optimal criterion number 1 # Current objective function value: 499(1.371s) # Current objective function value: 245(1.64s) # Current objective function value: 231(1.79s) # Current objective function value: 229(1.917s) # Current objective function value: 228(2.043s) # Current objective function value: 226(2.136s) # Current objective function value: 225(2.258s) # Found optimal solution for the last criterion # -removed criteria value: 102 # Removed packages: [aspcud, chromium, clasp, dragonplayer, dvdauthor, dvdrip, empathy, exim4, exim4-base, exim4-daemon-light, ftp, gcc-4.6-base, gnome, gnome-accessibility, gnome-applets, gnome-common, gnome-core, gnome-desktop-environment, gnome-system-tools, gringo, gstreamer0.10-plugins-bad, gstreamer0.10-plugins-ugly, gtk-doc-tools, intltool, k3b, kde, kde-config-cddb, kde-full, kde-standard, kdeedu, kdemultimedia, kdemultimedia-kio-plugins, libdvdnav4, libdvdread4, libgstfarsight0.10-0, libio-socket-ssl-perl, libk3b6, libk3b6-extracodecs, libkcddb4, libnet-dbus-perl, liboobs-1-4, libparse-debcontrol-perl, libqtassistantclient4, libqtlocation1, libqtmultimediakit1, libqtsensors1, libqtwebkit4, libquadmath0, libreoffice, libreoffice-base, libreoffice-base-core, libreoffice-calc, libreoffice-common, libreoffice-core, libreoffice-draw, libreoffice-emailmerge, libreoffice-filter-binfilter, libreoffice-filter-mobiledev, libreoffice-gnome, libreoffice-gtk, libreoffice-impress, libreoffice-java-common, libreoffice-math, libreoffice-officebean, libreoffice-report-builder-bin, libreoffice-style-galaxy, libreoffice-style-tango, libreoffice-writer, libsoap-lite-perl, libtelepathy-farsight0, libtextcat-data, libtextcat0, libwww-perl, libxine1, libxine1-misc-plugins, libxine1-plugins, libxml-parser-perl, libxml-sax-expat-perl, libxml-twig-perl, lsdvd, mccs, nautilus-sendto-empathy, netbase, nfs-common, parley, phonon-backend-xine, rinse, subtitleripper, system-tools-backends, telnet, transcode, virtualbox, virtualbox-dkms, virtualbox-qt, vlc, vlc-nox, vlc-plugin-notify, vlc-plugin-pulse, xine-ui, xserver-xorg-video-all, xserver-xorg-video-ark, xulrunner-5.0] # -changed criteria value: 225 # Changed packages: [apt, aspcud, avidemux, choqok, chromium, chromium-browser, chromium-browser-inspector, clasp, cpp-4.4, dma, dragonplayer, dvdauthor, dvdrip, empathy, exim4, exim4-base, exim4-daemon-light, ftp, g++-4.4, gcc-4.4, gcc-4.4-base, gcc-4.6-base, ghc, gnome, gnome-accessibility, gnome-applets, gnome-common, gnome-core, gnome-desktop-environment, gnome-system-tools, gringo, gstreamer0.10-plugins-bad, gstreamer0.10-plugins-ugly, gtk-doc-tools, iceweasel, intltool, k3b, kde, kde-config-cddb, kde-full, kde-standard, kdeedu, kdelibs-data, kdelibs4c2a, kdemultimedia, kdemultimedia-kio-plugins, knm-runtime, lib32gcc1, lib32stdc++6, libarts1c2a, libavahi-qt3-1, libbsd-dev, libc-bin, libc-dev-bin, libc6, libc6-dbg, libc6-dev, libc6-i386, libconfig-model-backend-augeas-perl, libconfig-model-perl, libdata-optlist-perl, libdevel-globaldestruction-perl, libdvdnav4, libdvdread4, libeval-closure-perl, libgcc1, libgfortran3, libghc-binary-dev, libghc-binary-shared-dev, libghc-cairo-dev, libghc-deepseq-dev, libghc-ghc-paths-dev, libghc-gio-dev, libghc-glib-dev, libghc-gtk-dev, libghc-haddock-dev, libghc-hslogger-dev, libghc-leksah-server-dev, libghc-ltk-dev, libghc-mtl-dev, libghc-network-dev, libghc-pango-dev, libghc-parsec3-dev, libghc-transformers-dev, libghc-xhtml-dev, libgmp-dev, libgomp1, libgstfarsight0.10-0, libid3-3.8.3c2a, libio-socket-ssl-perl, libk3b6, libk3b6-extracodecs, libkcddb4, liblua50, liblualib50, libmoose-perl, libnet-dbus-perl, liboobs-1-4, libpackage-deprecationmanager-perl, libpackage-stash-perl, libpackage-stash-xs-perl, libparams-util-perl, libparse-debcontrol-perl, libperl5.12, libqt4-assistant, libqt4-dbus, libqt4-designer, libqt4-help, libqt4-network, libqt4-opengl, libqt4-qt3support, libqt4-script, libqt4-scripttools, libqt4-sql, libqt4-sql-mysql, libqt4-sql-sqlite, libqt4-svg, libqt4-test, libqt4-webkit, libqt4-xml, libqt4-xmlpatterns, libqtassistantclient4, libqtcore4, libqtgui4, libqtlocation1, libqtmultimediakit1, libqtsensors1, libqtwebkit4, libquadmath0, libreoffice, libreoffice-base, libreoffice-base-core, libreoffice-calc, libreoffice-common, libreoffice-core, libreoffice-draw, libreoffice-emailmerge, libreoffice-filter-binfilter, libreoffice-filter-mobiledev, libreoffice-gnome, libreoffice-gtk, libreoffice-impress, libreoffice-java-common, libreoffice-math, libreoffice-officebean, libreoffice-report-builder-bin, libreoffice-style-galaxy, libreoffice-style-tango, libreoffice-writer, libshibsp-doc, libsoap-lite-perl, libstdc++6, libstdc++6-4.4-dev, libsub-exporter-perl, libsub-install-perl, libtelepathy-farsight0, libtextcat-data, libtextcat0, libtry-tiny-perl, libwps-0.1-1, libwww-perl, libxine1, libxine1-misc-plugins, libxine1-plugins, libxml-libxml-perl, libxml-parser-perl, libxml-sax-expat-perl, libxml-twig-perl, locales, lsdvd, mccs, nautilus-sendto-empathy, netbase, network-manager-kde, nfs-common, openoffice.org, openoffice.org-base, openoffice.org-base-core, openoffice.org-calc, openoffice.org-common, openoffice.org-core, openoffice.org-draw, openoffice.org-emailmerge, openoffice.org-filter-binfilter, openoffice.org-filter-mobiledev, openoffice.org-gnome, openoffice.org-gtk, openoffice.org-impress, openoffice.org-math, openoffice.org-officebean, openoffice.org-report-builder-bin, openoffice.org-style-galaxy, openoffice.org-style-tango, openoffice.org-writer, oss-compat, parley, perl, perl-base, perl-modules, phonon-backend-gstreamer, phonon-backend-xine, python-apt, python-uno, regina-normal, rinse, shishi-doc, subtitleripper, system-tools-backends, telnet, transcode, unetbootin, uno-libs3, ure, virtualbox, virtualbox-dkms, virtualbox-ose, virtualbox-qt, vlc, vlc-nox, vlc-plugin-notify, vlc-plugin-pulse, xine-ui, xserver-xorg-video-all, xserver-xorg-video-ark, xulrunner-5.0] # starts : 13 # conflicts : 678 # decisions : 255025 # propagations : 1695329 # inspects : 4177065 # shortcuts : 0 # learnt literals : 52 # learnt binary clauses : 151 # learnt ternary clauses : 56 # learnt constraints : 624 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 591 # 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) : 2.6909984126984127E7 # non guided choices 99590 # learnt constraints type # Solving done (4.858s). # The solution found IS optimal # Solution contains:2840