#Using input file /home/competition/data/random/rand.biglist/rand35d0c8.cudf #Using ouput file /home/competition/tmp/p2cudf-paranoid/rand35d0c8.cudf.rand.biglist.result #Objective function paranoid #Timeout 270s #java.runtime.name Java(TM) SE Runtime Environment #java.vm.name Java HotSpot(TM) Server VM #java.vm.version 11.2-b01 #java.vm.vendor Sun Microsystems Inc. #sun.arch.data.model 32 #java.version 1.6.0_12 #os.name Linux #os.version 2.6.18-6-xen-amd64 #os.arch i386 #Free memory 720163024 #Max memory 723845120 #Total memory 723845120 #Number of processors 2 #Parsing ... #Time to parse:1550 #Parsing done (1.553s). #Solving ... #Request size: 631 #Number of packages after slice: 3328 #Slice efficiency: 94% ## Optimization to Pseudo Boolean adapter # Pseudo Boolean Optimization # --- Begin Solver configuration --- # Stops conflict analysis at the first Unique Implication Point # org.sat4j.pb.constraints.CompetResolutionPBMixedHTClauseCardConstrDataStructure@47393f # 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 phase appearing in latest learned clause taking into account the objective function # Expensive reason simplification # MiniSAT restarts strategy # Glucose learned constraints deletion strategy # timeout=270s # DB Simplification allowed=false # --- End Solver configuration --- # Optimization function: misc 2010 paranoid #p cnf 6185 27229 # Current objective function value: 40930(0.505s) # Current objective function value: 21601(1.017s) # Current objective function value: 5718(1.146s) # Current objective function value: 5703(1.323s) # Current objective function value: 5683(1.426s) # Current objective function value: 5667(1.475s) # Current objective function value: 5666(1.546s) # cleaning 2493 clauses out of 5000 with flag 5000/5000 # cleaning 4254 clauses out of 8507 with flag 11000/11000 # Current objective function value: 5665(12.718s) # Current objective function value: 5664(12.944s) # cleaning 5623 clauses out of 11253 with flag 18000/18000 # Current objective function value: 5663(15.41s) # cleaning 6816 clauses out of 13631 with flag 26001/26001 # cleaning 7901 clauses out of 15814 with flag 35000/35000 # cleaning 8957 clauses out of 17914 with flag 45001/45001 # cleaning 9979 clauses out of 19957 with flag 56001/56001 # cleaning 10988 clauses out of 21978 with flag 68001/68001 # cleaning 11995 clauses out of 23989 with flag 81000/81000 # cleaning 12998 clauses out of 25995 with flag 95001/95001 # cleaning 13998 clauses out of 27997 with flag 110001/110001 # cleaning 14994 clauses out of 29999 with flag 126001/126001 # cleaning 15999 clauses out of 32005 with flag 143001/143001 # cleaning 16993 clauses out of 34006 with flag 161001/161001 # cleaning 18007 clauses out of 36013 with flag 180001/180001 # cleaning 18996 clauses out of 38006 with flag 200001/200001 # cleaning 20005 clauses out of 40010 with flag 221001/221001 # cleaning 20995 clauses out of 42005 with flag 243001/243001 # cleaning 22005 clauses out of 44009 with flag 266000/266000 # cleaning 22999 clauses out of 46006 with flag 290002/290002 # cleaning 23999 clauses out of 48006 with flag 315001/315001 # Current objective function value: 5662(237.285s) # cleaning 25000 clauses out of 50006 with flag 341000/341000 # Current objective function value: 5661(253.913s) # Current objective function value: 5660(255.209s) # Current objective function value: 5659(268.007s) # starts : 82 # conflicts : 365242 # decisions : 966398 # propagations : 328520142 # inspects : 864933836 # learnt literals : 0 # learnt binary clauses : 571 # learnt ternary clauses : 108 # learnt clauses : 365242 # ignored clauses : 0 # root simplifications : 0 # removed literals (reason simplification) : 57148922 # reason swapping (by a shorter reason) : 0 # Calls to reduceDB : 22 # 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) : 1.430213939921637E8 # non guided choices 9279 # learnt constraints type #Solving done (271.199s). #Solution contains:899