# Solver launched on Mon Sep 03 06:39:41 UTC 2012 # Using input file /home/competition/data/upgrade/difficult/rand491.cudf # Using ouput file /tmp/misc2012/2012-09-02-22:42/full/p2cudf-full-1.15/trendy-size/upgrade/difficult/rand491.cudf.result # Objective function -count(removed),-sum(solution,installedsize),-notuptodate(solution),-unsat_recommends(solution),-count(new) # 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:7541 # Parsing done (7.547s). # Solving ... # Request size: 1027 # Number of packages after slice: 13329 # Slice efficiency: 84% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@fee4648 # 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:-count(removed),-sum(solution,installedsize),-notuptodate(solution),-unsat_recommends(solution),-count(new) # criteria removed size is 950 using new vars 18158 to 19108 # criteria sum(installedsize) size is 0 Skipping unknown criteria:-notuptodate() # criteria notuptodate() size is 0 using new vars 19108 to 19108 Skipping unknown criteria:-unsat_recommends() # criteria unsat_recommends() size is 0 using new vars 19108 to 19108 # criteria new size is 4436 using new vars 19108 to 23544 # p cnf 23543 123367 # Current objective function value: 28(0.969s) # Current objective function value: 27(1.371s) # Current objective function value: 13(1.598s) # Found optimal criterion number 1 # Found optimal criterion number 2 # Current objective function value: 0(1.615s) # Found optimal criterion number 3 # Current objective function value: 0(1.957s) # Found optimal criterion number 4 # Current objective function value: 72(2.115s) # Current objective function value: 74(2.301s) # Current objective function value: 70(2.421s) # Current objective function value: 65(2.483s) # Found optimal solution for the last criterion # -removed criteria value: 13 # Removed packages: [exim4, exim4-base, exim4-daemon-light, gdm, hotplug, kde, kdegraphics, kuickshow, libdps1, libmagick6, libostyle1, libungif4g, linux-kernel-headers] # -sum(installedsize) criteria value: 0 # -new criteria value: 65 # Newly installed packages: [bzr, bzr-svn, dbus, dma, fontconfig-config, gcc-4.4-base, libapr1, libaprutil1, libc-bin, libc-dev-bin, libcairo2, libcairo2-dev, libdb4.8, libdbus-1-3, libdbus-glib-1-2, libfs6, libgif4, libgnutls26, libgssapi-krb5-2, libhal-storage1, libhal1, libk5crypto3, libkeyutils1, libkrb5-3, libkrb5support0, libldap-2.4-2, libmagick9, libncursesw5, libneon27-gnutls, libosp5, libostyle1c2, libreadline6, libsasl2-2, libserf-0-0, libsqlite3-0, libssl0.9.8, libstdc++6, libsvn1, libtasn1-3, libuptimed0, libvolume-id0, libxau6, libxkbfile1, libxss1, libxxf86dga1, libxxf86vm1, licq, licq-plugin-console, linux-libc-dev, lsb-base, python-central, python-configobj, python-minimal, python-subvertpy, python-support, python2.5, python2.5-minimal, python2.6, python2.6-minimal, readline-common, reglookup, uptimed, x11-common, x11proto-core-dev, xine-ui] # starts : 10 # conflicts : 634 # decisions : 513507 # propagations : 3189819 # inspects : 9103387 # shortcuts : 0 # learnt literals : 42 # learnt binary clauses : 282 # learnt ternary clauses : 74 # learnt constraints : 590 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 193 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 0 # Number of update (reduction) of LBD : 119 # 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) : 1114931.4924851449 # non guided choices 396088 # learnt constraints type # Solving done (7.023s). # The solution found IS optimal # Solution contains:1002