# Solver launched on Mon Sep 03 09:24:14 UTC 2012
# Using input file /home/competition/data/upgrade/easy/rand381.cudf
# Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/slowlink/upgrade/easy/rand381.cudf.result
# Objective function -sum(changed,installedsize),-count(removed),-notuptodate(solution),-count(changed)
# Timeout 285s
# java.runtime.name	OpenJDK Runtime Environment
# java.vm.name		OpenJDK 64-Bit Server VM
# java.vm.version	20.0-b12
# java.vm.vendor	Sun Microsystems Inc.
# sun.arch.data.model	64
# java.version		1.6.0_24
# os.name		Linux
# os.version		2.6.32-5-amd64
# os.arch		amd64
# Free memory 		655262992
# Max memory 		658898944
# Total memory 		658898944
# Number of processors 	1
# Parsing ...
# Time to parse:5415
# Parsing done (5.444s).
# Solving ...
# Request size: 1012
# Number of  packages after slice: 5192
# Slice efficiency: 91%
# --- Begin Solver configuration ---
# org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@687b6889
# 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 2 learned constraints deletion strategy
# timeout=285s
# DB Simplification allowed=false
# --- End Solver configuration ---
# Optimization function: User defined:-sum(changed,installedsize),-count(removed),-notuptodate(solution),-count(changed)
# criteria sum(changed,installedsize) size is 0
# criteria removed size is 950 using new vars 6143 to 7093
Skipping unknown criteria:-notuptodate()
# criteria notuptodate() size is 950 using new vars 7093 to 7093
# criteria changed size is 5191 using new vars 7093 to 7093
# p cnf 7092 46106
# Found optimal criterion number 1
# Current objective function value: 17(0.265s)
# Current objective function value: 17(0.411s)
# Found optimal criterion number 2
# Current objective function value: 17(0.449s)
# Found optimal criterion number 3
# Current objective function value: 25(0.569s)
# Found optimal solution for the last criterion 
# -sum(changed,installedsize) criteria value: 0
# -removed criteria value: 17
# Removed packages: [cervisia, gnome, gnome-applets, gnome-core, gnome-desktop-environment, gnome-office, gnome-system-monitor, gnome-volume-manager, gstreamer0.8-oss, hal, kde-devel, kde-devel-extras, kdesdk, libgtop2-2, libmlgtk-ocaml, libmlgtk-ocaml-dev, udev]
# -changed criteria value: 25
# Changed packages: [-cervisia 20301, -gnome 17322, -gnome-applets 13017, -gnome-core 17322, -gnome-desktop-environment 17322, -gnome-office 17322, -gnome-system-monitor 13003, -gnome-volume-manager 7583, gstreamer0.8-esd 3206, -gstreamer0.8-oss 3206, -hal 1907, -kde-devel 20441, -kde-devel-extras 20442, -kdesdk 20301, -libgtop2-2 12581, -libmlgtk-ocaml 10943, -libmlgtk-ocaml-dev 10943, libstring-crc32-perl 7480, libtk-img 18870, libtmail-ruby-doc 3971, liburi-find-delimited-perl 879, liburi-find-perl 4308, python-dnspython 8200, python-support 2234, -udev 5141]
# starts		: 3
# conflicts		: 43
# decisions		: 4751
# propagations		: 42797
# inspects		: 262983
# shortcuts		: 0
# learnt literals	: 5
# learnt binary clauses	: 4
# learnt ternary clauses	: 6
# learnt constraints	: 37
# ignored constraints	: 0
# root simplifications	: 0
# removed literals (reason simplification)	: 9
# reason swapping (by a shorter reason)	: 0
# Calls to reduceDB	: 0
# Number of update (reduction) of LBD	: 3
# 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)	: 57833.78378378379
# non guided choices	3770
# learnt constraints type 
# Solving done (4.481s).
# The solution found IS optimal
# Solution contains:941