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:31:07 CEST 2011 # Using input file /home/misc2010/data/2011/incremental/s/rand586.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand586.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:1642 # Parsing done (1.645s). # Solving ... # Request size: 992 # Number of packages after slice: 1320 # Slice efficiency: 92% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@a8c488 # 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 2271 to 3221 # criteria changed size is 1319 using new vars 3221 to 4540 # p cnf 4539 15741 # Current objective function value: 48(0.144s) # Found optimal criterion number 1 # Current objective function value: 86(0.264s) # Current objective function value: 84(0.463s) # Found optimal solution for the last criterion # -removed criteria value: 48 # Removed packages: [capplets, evolution, gnome, gnome-applets, gnome-control-center, gnome-core, gnome-desktop-environment, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnome-terminal, gtkhtml3.2, kde, kde-amusements, kde-core, kde-devel, kde-devel-extras, kdeaddons, kdebase, kdebase-dev, kdeedu, kdelibs4-dev, kdemultimedia, kdenetwork, kdesdk, klipper, knewsticker-scripts, kopete, ksplash, kspy, ktouch, kvoctrain, libarts1-audiofile, libarts1-dev, libartsc0-dev, libfinance-quote-perl, libgtkhtml3.2-11, libhtml-tree-perl, libkonq4-dev, libnautilus2-2, libwww-perl, nautilus, nautilus-cd-burner, nautilus-media, x-window-system-core, xlibmesa-glu, xlibmesa-glu-dev] # -changed criteria value: 84 # Changed packages: [aspell-tl, capplets, debconf-utils, debhelper, dia, dialog, dpkg-dev, ecasound, ecasound-el, emacs21-bin-common, emacs21-common, emacs21-nox, emacsen-common, evolution, gnome, gnome-applets, gnome-control-center, gnome-core, gnome-desktop-environment, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnome-terminal, gtkhtml3.2, gtkmorph-example, html2text, intltool-debian, kde, kde-amusements, kde-core, kde-devel, kde-devel-extras, kdeaddons, kdebase, kdebase-dev, kdeedu, kdelibs4-dev, kdemultimedia, kdenetwork, kdesdk, klipper, knewsticker-scripts, kopete, ksplash, kspy, ktouch, kvoctrain, libarts1-audiofile, libarts1-dev, libartsc0-dev, libdb2, libfinance-quote-perl, libgatos0, libglu1-mesa, libglu1-mesa-dev, libgtkhtml3.2-11, libhtml-tree-perl, libkonq4-dev, libmorph, libnautilus2-2, libncursesw5, libsndfile1, libwww-perl, lockfile-progs, logcheck, logcheck-database, logtail, make, mknbi, module-assistant, nautilus, nautilus-cd-burner, nautilus-media, patch, po-debconf, python-ecasound2.2, skkdic, skksearch, translucency-source, x-window-system-core, xlibmesa-glu, xlibmesa-glu-dev, xmorph] # starts : 4 # conflicts : 46 # decisions : 8268 # propagations : 46773 # inspects : 131370 # shortcuts : 0 # learnt literals : 23 # learnt binary clauses : 1 # learnt ternary clauses : 0 # learnt constraints : 21 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 1 # 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) : 2338650.0 # non guided choices 2058 # learnt constraints type # Solving done (2.182s). # The solution found IS optimal # Solution contains:938