# 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:01:21 CEST 2011 # Using input file /home/misc2010/data/2011/incremental/s/rand0.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand0.cudf.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:1514 # Parsing done (1.516s). # Solving ... # Request size: 992 # Number of packages after slice: 1300 # Slice efficiency: 92% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@12d7a10 # 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 2251 to 3201 # criteria changed size is 1299 using new vars 3201 to 4500 # p cnf 4499 15463 # Current objective function value: 115(0.807s) # Found optimal criterion number 1 # Current objective function value: 151(0.824s) # Found optimal solution for the last criterion # -removed criteria value: 115 # Removed packages: [abiword-gnome, bluefish, bug-buddy, capplets, capplets-data, dia-gnome, docbook-dsssl, docbook-xml, eog, epiphany-browser, evolution, evolution-data-server, file-roller, gcalctool, gconf-editor, gdm, gedit, gedit-common, gnome, gnome-about, gnome-applets, gnome-applets-data, gnome-control-center, gnome-core, gnome-cups-manager, gnome-desktop-environment, gnome-doc-tools, gnome-games, gnome-gv, gnome-icon-theme, gnome-media, gnome-nettool, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnome-system-monitor, gnome-system-tools, gnome-terminal, gnome-themes, gnome-utils, gnome-volume-manager, gnome2-user-guide, gnomemeeting, gnumeric, gnumeric-common, gpdf, gstreamer0.8-gnomevfs, gtk2-engines-mist, gtkhtml3.2, gucharmap, kde, kde-amusements, kde-core, kde-devel, kde-devel-extras, kdeartwork, kdeartwork-misc, kdegraphics, kdelibs, kdesdk, kdesdk-misc, kghostview, libbonobo2-0, libbonobo2-common, libbonobo2-dev, libbonoboui2-0, libbonoboui2-dev, libcompfaceg1, libebook8, libecal6, libedata-book1, libedata-cal5, libedataserver3, libeel2-2, libegroupwise6, libgal2.2-1, libgal2.2-common, libgnome-desktop-2, libgnome2-0, libgnome2-dev, libgnomecupsui1.0-1, libgnomeui-0, libgnomeui-dev, libgnomevfs2-0, libgnomevfs2-common, libgnomevfs2-dev, libgsf-gnome-1, libgtkhtml3.2-11, liblablgtk2-ocaml, liblablgtk2-ocaml-dev, libnautilus2-2, libpanel-applet2-0, libpanel-applet2-dev, nautilus, nautilus-cd-burner, nautilus-data, nautilus-media, openoffice.org, openoffice.org-bin, openoffice.org-debian-files, planner, rhythmbox, scrollkeeper, sgml-data, synaptic, totem, totem-xine, vino, x-window-system-core, xlibmesa-glu, xlibmesa-glu-dev, xml-core, yelp, zenity] # -changed criteria value: 151 # Changed packages: [abiword, abiword-gnome, acl, bluefish, bug-buddy, capplets, capplets-data, dia-gnome, docbook-dsssl, docbook-xml, eog, epiphany-browser, evolution, evolution-data-server, file-roller, freeglut3-dev, gawk, gcalctool, gconf-editor, gdm, gedit, gedit-common, gnome, gnome-about, gnome-applets, gnome-applets-data, gnome-control-center, gnome-core, gnome-cups-manager, gnome-desktop-environment, gnome-doc-tools, gnome-games, gnome-gv, gnome-icon-theme, gnome-media, gnome-nettool, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnome-system-monitor, gnome-system-tools, gnome-terminal, gnome-themes, gnome-utils, gnome-volume-manager, gnome2-user-guide, gnomemeeting, gnumeric, gnumeric-common, gnustep-make-ogo, gpdf, gstreamer0.8-gnomevfs, gtk2-engines-mist, gtkhtml3.2, gucharmap, kde, kde-amusements, kde-core, kde-devel, kde-devel-extras, kdeartwork, kdeartwork-misc, kdegraphics, kdelibs, kdesdk, kdesdk-misc, kghostview, ksymoops, lg-base, lg-issue32, libauthen-pam-perl, libbonobo2-0, libbonobo2-common, libbonobo2-dev, libbonoboui2-0, libbonoboui2-dev, libcompfaceg1, libconvert-ber-perl, libebook8, libecal6, libedata-book1, libedata-cal5, libedataserver3, libeel2-2, libegroupwise6, libgal2.2-1, libgal2.2-common, libglu1-mesa, libglu1-mesa-dev, libglut3-dev, libgnome-desktop-2, libgnome2-0, libgnome2-dev, libgnomecupsui1.0-1, libgnomeui-0, libgnomeui-dev, libgnomevfs2-0, libgnomevfs2-common, libgnomevfs2-dev, libgsf-gnome-1, libgtkhtml3.2-11, liblablgtk2-ocaml, liblablgtk2-ocaml-dev, libmd5-perl, libmon-perl, libnautilus2-2, libnet-ssleay-perl, libpanel-applet2-0, libpanel-applet2-dev, libsdl-image1.2, libsdl-mixer1.2, libsdl-ocaml, libsdl-ocaml-dev, libsdl-ttf2.0-0, libsmpeg0, libsys-hostname-long-perl, libtime-period-perl, man2html, mon, nautilus, nautilus-cd-burner, nautilus-data, nautilus-media, openoffice.org, openoffice.org-bin, openoffice.org-debian-files, openssl, planner, plib1.8.3, plib1.8.3-dev, rhythmbox, scrollkeeper, sgml-data, simgear-dev, simgear0, solid-pop3d, synaptic, totem, totem-xine, vino, webmin, webmin-core, webmin-mon, x-window-system-core, xfonts-cronyx-cp1251-100dpi, xlibmesa-glu, xlibmesa-glu-dev, xml-core, yelp, zenity] # starts : 2 # conflicts : 22 # decisions : 6471 # propagations : 36894 # inspects : 99483 # shortcuts : 0 # learnt literals : 21 # learnt binary clauses : 0 # learnt ternary clauses : 0 # learnt constraints : 0 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 0 # 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) : 323631.5789473684 # non guided choices 1069 # learnt constraints type # Solving done (2.85s). # The solution found IS optimal # Solution contains:871