HEAD is now at 2b6ae8b initial deployement # 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:47:38 CEST 2011 # Using input file /home/misc2010/data/2011/dudf-random/rand282.cudf # Using ouput file /home/misc2010/tmp/201108251442/p2cudf-paranoid-1.13/rand282.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:3009 # Parsing done (3.012s). # Solving ... # Request size: 2942 # Number of packages after slice: 7677 # Slice efficiency: 88% # --- Begin Solver configuration --- # org.sat4j.pb.constraints.CompetResolutionPBLongMixedWLClauseCardConstrDataStructure@152544e # 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 2892 using new vars 10570 to 13462 # criteria changed size is 3951 using new vars 13462 to 17413 # p cnf 17412 79231 # Current objective function value: 9(0.503s) # Found optimal criterion number 1 # Current objective function value: 300(0.642s) # Current objective function value: 32(1.002s) # Current objective function value: 31(1.158s) # Found optimal solution for the last criterion # -removed criteria value: 9 # Removed packages: [kdesdk, kdesdk-kio-plugins, libeina-svn-06, libpostgresql-ocaml, libpostgresql-ocaml-dev, libsdl-mixer1.2, libsdl-ocaml, libsvn1, subversion] # -changed criteria value: 31 # Changed packages: [ghc, ghc-haddock, gobby-0.5, gobby-infinote, kdesdk, kdesdk-kio-plugins, libbsd-dev, libeet1, libeina-svn-06, libeina1, libghc-tagged-doc, libgmp-dev, libgsasl7, libhocr-dev, libhocr0, libinfgtk-0.5-0, libinfinity-0.5-0, libjpeg8, libntl-5.4.2, libntlm0, libpostgresql-ocaml, libpostgresql-ocaml-dev, libsdl-mixer1.2, libsdl-ocaml, libsingular-3-0-4-3, libsvn1, libxml++2.6-2, pike7.8-bzip2, pike7.8-core, singular, subversion] # starts : 4 # conflicts : 55 # decisions : 74931 # propagations : 386297 # inspects : 1222063 # shortcuts : 0 # learnt literals : 26 # learnt binary clauses : 21 # learnt ternary clauses : 5 # learnt constraints : 28 # ignored constraints : 0 # root simplifications : 0 # removed literals (reason simplification) : 1 # 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) : 8584377.777777778 # non guided choices 21444 # learnt constraints type # Solving done (3.735s). # The solution found IS optimal # Solution contains:2903