# Solver launched on Mon Sep 03 09:19:11 UTC 2012 # Using input file /home/competition/data/upgrade/easy/rand261.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/slowlink/upgrade/easy/rand261.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:5405 # Parsing done (5.412s). # Solving ... # Request size: 1012 # Number of packages after slice: 5203 # Slice efficiency: 91% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@5a5e5a50 # 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 6154 to 7104 Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 950 using new vars 7104 to 7104 # criteria changed size is 5202 using new vars 7104 to 7104 # p cnf 7103 46165 # Found optimal criterion number 1 # Current objective function value: 14(0.303s) # Current objective function value: 14(0.375s) # Found optimal criterion number 2 # Current objective function value: 14(0.409s) # Found optimal criterion number 3 # Current objective function value: 83(0.478s) # cleaning 2499 clauses out of 4997 with flag 10169/5010 # cleaning 4249 clauses out of 8498 with flag 22242/11010 # cleaning 5616 clauses out of 11250 with flag 36289/18011 # cleaning 6817 clauses out of 13633 with flag 52393/26010 # cleaning 7903 clauses out of 15814 with flag 70712/35010 # cleaning 8956 clauses out of 17912 with flag 90865/45011 # cleaning 9977 clauses out of 19953 with flag 113119/56010 # cleaning 10987 clauses out of 21976 with flag 137423/68010 # cleaning 11993 clauses out of 23989 with flag 163678/81010 # cleaning 12994 clauses out of 25996 with flag 191867/95010 # cleaning 13996 clauses out of 28002 with flag 222275/110010 # cleaning 15000 clauses out of 30007 with flag 254723/126011 # cleaning 16001 clauses out of 32007 with flag 289074/143011 # cleaning 16996 clauses out of 34005 with flag 325591/161010 # cleaning 18001 clauses out of 36010 with flag 364037/180011 # cleaning 19002 clauses out of 38008 with flag 404453/200010 # Found optimal solution for the last criterion # -sum(changed,installedsize) criteria value: 0 # -removed criteria value: 14 # Removed packages: [cpp-3.3, gcc-3.3-base, gdm, gksu, kde, kde-amusements, kdeaddons, kdegames, kdegraphics, kmines, knewsticker-scripts, libio-stringy-perl, libmime-perl, linux-kernel-headers] # -changed criteria value: 83 # Changed packages: [-binutils 13428, binutils 13502, -cpp 20312, cpp 20407, -cpp-3.3 19585, cpp-4.1 15475, -fontconfig 11990, fontconfig 12579, fontconfig-config 12253, -gcc-3.3-base 19585, gcc-4.1-base 15475, -gdm 12586, -gksu 7757, -kde 20441, -kde-amusements 20441, -kdeaddons 20303, -kdegames 20295, -kdegraphics 20300, -kmines 20295, -knewsticker-scripts 20303, libalgorithm-diff-ruby1.8 1665, -libc6 12041, libc6 12852, -libc6-dev 12041, libc6-dev 12852, libcairo2 7741, libcairo2-dev 7741, libdb4.3 15693, -libfontconfig1 11990, libfontconfig1 12253, -libfontconfig1-dev 11990, libfontconfig1-dev 12253, -libfreetype6 11530, libfreetype6 11738, -libfreetype6-dev 11530, libfreetype6-dev 11738, -libgcc1 19603, libgcc1 19690, -libgcrypt11 7605, libgcrypt11 7718, -libgcrypt11-dev 7605, libgcrypt11-dev 7718, -libglib2.0-0 12633, libglib2.0-0 13307, -libglib2.0-dev 12633, libglib2.0-dev 13307, -libgpg-error-dev 6264, libgpg-error-dev 8337, -libgpg-error0 6264, libgpg-error0 8337, -libio-stringy-perl 13889, -libmime-perl 16528, libmysqlclient12 15417, -libpango1.0-0 9332, libpango1.0-0 9885, -libpango1.0-common 9332, libpango1.0-common 9885, -libpango1.0-dev 9332, libpango1.0-dev 9885, libpcap0.8 3120, -libpng12-0 7841, libpng12-0 7919, -libpng12-dev 7841, libpng12-dev 7919, libruby1.8 9358, libsmtpguard1 7234, -libstdc++5 19585, libstdc++5 19590, -libxml2 12701, libxml2 12830, -libxml2-dev 12701, libxml2-dev 12830, -libxslt1.1 7363, libxslt1.1 7400, -linux-kernel-headers 12531, linux-libc-dev 12811, mysql-common 16092, python-gnome2-dev 12589, smtpguard 7234, snort-common 12026, snort-mysql 12026, snort-rules-default 12052, ttf-kacst 8666] # starts : 129 # conflicts : 206391 # decisions : 242860 # propagations : 178349002 # inspects : 693832403 # shortcuts : 0 # learnt literals : 19 # learnt binary clauses : 23 # learnt ternary clauses : 18 # learnt constraints : 206371 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 3162885 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 16 # Number of update (reduction) of LBD : 1575 # 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) : 1092858.2493336194 # non guided choices 10278 # learnt constraints type # Solving done (165.842s). # The solution found IS optimal # Solution contains:955