# 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:25:11 CEST 2011 # Using input file /home/misc2010/data/2011/incremental/s/rand144.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand144.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:1662 # Parsing done (1.665s). # Solving ... # Request size: 992 # Number of packages after slice: 1286 # Slice efficiency: 92% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@143c8b3 # 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 2237 to 3187 # criteria changed size is 1285 using new vars 3187 to 4472 # p cnf 4471 15391 # Current objective function value: 41(0.139s) # Found optimal criterion number 1 # Current objective function value: 61(0.182s) # Found optimal solution for the last criterion # -removed criteria value: 41 # Removed packages: [capplets, dirmngr, epiphany-browser, g++-2.95, gedit, gedit-common, gnome, gnome-applets, gnome-control-center, gnome-core, gnome-desktop-environment, gnome-games, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnome-terminal, gnupg-agent, guile-1.6-libs, kate-plugins, kde, kde-amusements, kdeaddons, kdeedu, kdepim, kdewebdev, kleopatra, kstars, libeel2-2, libeel2-data, libnautilus2-2, libpth2, libstdc++2.10-dev, mozilla-psm, nautilus, nautilus-cd-burner, nautilus-media, quanta, tidy, x-window-system-core, xfonts-base] # -changed criteria value: 61 # Changed packages: [bigloo-examples, capplets, dirmngr, doc-linux-pl, epiphany-browser, g++-2.95, g++-3.3, gcc-3.3, gedit, gedit-common, gnome, gnome-applets, gnome-control-center, gnome-core, gnome-desktop-environment, gnome-games, gnome-office, gnome-panel, gnome-panel-data, gnome-session, gnome-terminal, gnupg-agent, guile-1.6-libs, kate-plugins, kde, kde-amusements, kdeaddons, kdeedu, kdepim, kdewebdev, kleopatra, kstars, libdevice-serialport-perl, libeel2-2, libeel2-data, libnautilus2-2, libnet-snpp-perl, libocamlnet-ocaml, libocamlnet-ocaml-dev, libpcre-ocaml, libpcre-ocaml-dev, libpth2, libpxp-ocaml-dev, libstdc++2.10-dev, libstdc++5-3.3-dev, mozilla-psm, nautilus, nautilus-cd-burner, nautilus-media, ocaml-findlib, ocaml-ulex, quanta, sendpage-common, tidy, ttfprint, w3-dtd-mathml, x-window-system-core, xchat-common, xchat-text, xfonts-base, xtide] # starts : 2 # conflicts : 18 # decisions : 5217 # propagations : 31142 # inspects : 84793 # shortcuts : 0 # learnt literals : 17 # 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) : 191055.2147239264 # non guided choices 1124 # learnt constraints type # Solving done (2.025s). # The solution found IS optimal # Solution contains:929