# 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 720172360 # Max memory 723845120 # Total memory 723845120 # Number of processors 2 # Using input file /home/competition/data/random/rand.newlist/rand5d20db.cudf # Using output file /home/competition/tmp/p2cudf-paranoid/rand5d20db.cudf.rand.newlist.result # Using criteria paranoid # Parsing ... # Parsing done (2.652s). # Solving ... # Starting projection ... # 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@a46701 # 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 # No reason simplification # MiniSAT restarts strategy # Memory based learned constraints deletion strategy # timeout=270s # DB Simplification allowed=false # --- End Solver configuration --- # Optimization function: misc 2010 paranoid # Projection completed: 825ms. # Invoking solver ... # Solver first solution found: 1268ms. # Current objective function value: 13149(1.274s) # Current objective function value: 8339(1.82s) # Current objective function value: 8328(2.079s) # Current objective function value: 6761(2.18s) # Current objective function value: 6746(2.268s) # Current objective function value: 6745(2.361s) # Current objective function value: 6744(2.525s) # Current objective function value: 6743(2.619s) # Current objective function value: 6742(2.699s) # Current objective function value: 6741(2.808s) # Current objective function value: 6740(2.959s) # Current objective function value: 6735(3.073s) # Current objective function value: 6734(3.299s) # Current objective function value: 6733(3.623s) # Current objective function value: 5228(3.859s) # Current objective function value: 5121(3.935s) # Current objective function value: 5118(4.01s) # Current objective function value: 5117(4.094s) # Current objective function value: 5116(4.199s) # Current objective function value: 5115(4.274s) # Current objective function value: 5114(4.358s) # Current objective function value: 5113(5.652s) # Current objective function value: 5112(5.848s) # Current objective function value: 5109(6.036s) # Current objective function value: 5108(6.12s) # Current objective function value: 5107(6.667s) # Solver best solution decoded: 6725ms. # p cnf 31934 26188 # starts : 46 # conflicts : 5272 # decisions : 185427 # propagations : 4080952 # inspects : 8138675 # learnt literals : 0 # learnt binary clauses : 0 # learnt ternary clauses : 0 # learnt clauses : 5271 # ignored clauses : 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) : 8.001866666666667E7 # non guided choices 16882 # learnt constraints type # Solving done (8.443s). # Solution contains:796