# 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:27:40 CEST 2011 # Using input file /home/misc2010/data/2011/dudf-random/rand399.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand399.cudf.dudf-random.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:2295 # Parsing done (2.298s). # Solving ... # Request size: 1621 # Number of packages after slice: 2057 # Slice efficiency: 95% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@1feca64 # 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 1572 using new vars 3630 to 5202 # criteria changed size is 1727 using new vars 5202 to 6929 # p cnf 6928 17595 # Current objective function value: 20(0.167s) # Found optimal criterion number 1 # Current objective function value: 47(0.277s) # Current objective function value: 30(0.391s) # Found optimal solution for the last criterion # -removed criteria value: 20 # Removed packages: [ia32-libs, libdate-manip-perl, libdbd-mysql-perl, libdbi-perl, libgail-dev, libglade2-dev, libgnomecanvas2-dev, libgtk2.0-dev, libgtkspell-dev, liblablgtk2-ocaml-dev, libnet-daemon-perl, libocsigen-ocaml-doc, libplrpc-perl, librsvg2-dev, libsql-translator-perl, libxml2-utils, libyaml-syck-perl, mysql-client, mysql-client-5.1, sqlfairy] # -changed criteria value: 30 # Changed packages: [bobot++, fairymax, guile-1.6-libs, ia32-libs, libdate-manip-perl, libdbd-mysql-perl, libdbi-perl, libgail-dev, libglade2-dev, libglibmm-2.4-1c2a, libgnomecanvas2-dev, libgtk2.0-dev, libgtkspell-dev, libguile-ltdl-1, liblablgtk2-ocaml-dev, liblircclient-dev, liblircclient0, libnet-daemon-perl, libocsigen-ocaml-doc, libplrpc-perl, librsvg2-dev, libsql-translator-perl, libxml2-utils, libyaml-syck-perl, mysql-client, mysql-client-5.1, sqlfairy, tdb-tools, tmispell-voikko, voikko-fi] # starts : 2 # conflicts : 12 # decisions : 9754 # propagations : 48706 # inspects : 114490 # shortcuts : 0 # learnt literals : 12 # 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) : 2705888.888888889 # non guided choices 3382 # learnt constraints type # Solving done (2.077s). # The solution found IS optimal # Solution contains:1562