# 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:00:40 CEST 2011 # Using input file /home/misc2010/data/2011/incremental/s-e-l/rand115.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand115.cudf.s-e-l.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:2481 # Parsing done (2.484s). # Solving ... # Request size: 992 # Number of packages after slice: 5255 # 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 6206 to 7156 # criteria changed size is 2463 using new vars 7156 to 9619 # p cnf 9618 54273 # Current objective function value: 449(0.465s) # Current objective function value: 115(0.591s) # Current objective function value: 114(0.852s) # Current objective function value: 109(0.932s) # Current objective function value: 98(1.031s) # Current objective function value: 93(1.124s) # Found optimal criterion number 1 # Current objective function value: 215(1.166s) # Current objective function value: 205(1.412s) # Current objective function value: 193(1.503s) # Current objective function value: 191(1.607s) # Found optimal solution for the last criterion # -removed criteria value: 93 # Removed packages: [adduser, base-config, capplets, cron, dbus-1, dbus-glib-1, dirmngr, exim4, exim4-base, exim4-config, exim4-daemon-light, freeglut3, gdm, gnome, gnome-applets, gnome-control-center, gnome-core, gnome-desktop-environment, gnome-games, gnome-media, gnome-office, gnome-panel, gnome-session, gnome-terminal, gnome-themes-extras, gnome-volume-manager, gnupg, gpgsm, gstreamer0.8-flac, gstreamer0.8-misc, gstreamer0.8-vorbis, gtk2-engines-spherecrystal, hal, kaddressbook, kaddressbook-plugins, kamera, kde, kde-devel, kde-devel-extras, kdeaddons, kdebase-dev, kdegraphics, kdelibs4-dev, kdenetwork, kdepim, kdepim-wizards, kdesdk, kdessh, kdeutils, kgpg, kleopatra, kmail, kmailcvt, kooka, korganizer, ksirc, kspy, ktimer, libarts1-dev, libartsc0-dev, libglut3, libgpgme11, libgphoto2-2, libgphoto2-port0, libgstreamer-gconf0.8-0, libhal-storage0, libhal0, libkleopatra0a, libkonq4-dev, libkpimidentities1, libkscan1, liblablgl-ocaml, liblablgl-ocaml-dev, liblablgtk2-ocaml, liblablgtk2-ocaml-dev, libnautilus-burn0, libnautilus2-2, librsvg2-2, librsvg2-common, librsvg2-dev, libsane, libusb-0.1-4, linux-kernel-headers, nautilus, nautilus-cd-burner, nautilus-media, passwd, rhythmbox, sane-utils, ssh, totem, totem-xine, usbutils] # -changed criteria value: 191 # Changed packages: [adduser, anacron, apache2-doc, aqbanking-tool, aqbanking-tools, base-config, bash, binutils, capplets, cron, dbus-1, dbus-glib-1, debianutils, dirmngr, exim4, exim4-base, exim4-config, exim4-daemon-light, fontconfig, fontconfig-config, fping, freeglut3, gcc-4.3-base, gconf2, gconf2-common, gdm, gnome, gnome-applets, gnome-control-center, gnome-core, gnome-desktop-environment, gnome-games, gnome-media, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnome-terminal, gnome-themes-extras, gnome-volume-manager, gnupg, gpgsm, gstreamer0.8-flac, gstreamer0.8-misc, gstreamer0.8-vorbis, gtk2-engines-spherecrystal, hal, kaddressbook, kaddressbook-plugins, kamera, kde, kde-devel, kde-devel-extras, kdeaddons, kdebase-dev, kdegraphics, kdelibs4-dev, kdenetwork, kdepim, kdepim-wizards, kdesdk, kdessh, kdeutils, kgpg, kleopatra, kmail, kmailcvt, kooka, korganizer, ksirc, kspy, ktimer, libaqbanking-data, libaqbanking20, libaqhbci13, libarts1-dev, libartsc0-dev, libc6, libc6-dev, libcairo2, libcairo2-dev, libdbus-1-3, libdisplaymigration0, libeventdb-dev, libeventdb2, libfontconfig1, libfontconfig1-dev, libfreetype6, libfreetype6-dev, libgcc1, libgconf2-4, libgconf2-dev, libgcrypt11, libgcrypt11-dev, libglib2.0-0, libglib2.0-dev, libglut3, libgmp3c2, libgnutls26, libgpepimc0, libgpevtype-dev, libgpevtype1, libgpewidget1, libgpg-error-dev, libgpg-error0, libgpgme11, libgphoto2-2, libgphoto2-port0, libgstreamer-gconf0.8-0, libgtkextra-dev, libgtkextra16, libgwenhywfar47, libhal-storage0, libhal-storage1, libhal0, libhal1, libidl-dev, libidl0, libkleopatra0a, libkonq4-dev, libkpimidentities1, libkscan1, liblablgl-ocaml, liblablgl-ocaml-dev, liblablgtk2-ocaml, liblablgtk2-ocaml-dev, libldap-2.4-2, libmimedir-gnome0-dev, libmimedir-gnome0.4, libmysqlclient12, libnautilus-burn0, libnautilus2-2, libncurses5, libncurses5-dev, libopenct1, liborbit2, liborbit2-dev, libpango1.0-0, libpango1.0-common, libpango1.0-dev, libpcre3, libpcre3-dev, libpcrecpp0, libpng12-0, libpng12-dev, librsvg2-2, librsvg2-common, librsvg2-dev, libsane, libsasl2-2, libselinux1, libsqlite0, libstdc++6, libsysfs2, libtasn1-3, libtododb0, libuclmmbase1, libusb-0.1-4, libxml2, libxml2-dev, libxslt1.1, linux-kernel-headers, linux-libc-dev, mdnkit-doc-jp, mysql-common-4.1, nautilus, nautilus-cd-burner, nautilus-media, passwd, pmount, python-biopython-sql, python-mysqldb, python2.3-biopython, python2.3-biopython-martel, python2.3-biopython-sql, python2.3-egenix-mxtexttools, python2.3-egenix-mxtools, python2.3-mysqldb, python2.3-reportlab, python2.3-xml, rhythmbox, runit, runit-run, sane-utils, ssh, totem, totem-xine, tz-brasil, usbutils, xfonts-100dpi-transcoded, xmail] # starts : 11 # conflicts : 506 # decisions : 146792 # propagations : 863647 # inspects : 3185432 # shortcuts : 0 # learnt literals : 98 # learnt binary clauses : 216 # learnt ternary clauses : 53 # learnt constraints : 406 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 244 # 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) : 1.5422267857142856E7 # non guided choices 72296 # learnt constraints type # Solving done (3.906s). # The solution found IS optimal # Solution contains:915