Result page for benchmark mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-core4284-1064.opb

Jump to solvers results

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-core4284-1064.opb
MD5SUM15e353c3ac96932543c879f694fc1285
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1413120000000000
Optimality of the best value was proved NO
Number of terms in the objective function 21975
Biggest coefficient in the objective function 53687091200000000000
Number of bits for the biggest coefficient in the objective function 66
Sum of the numbers in the objective function 215753096412511174656
Number of bits of the sum of numbers in the objective function 68
Biggest number in a constraint 10240000000000000000000
Number of bits of the biggest number in a constraint 74
Biggest sum of numbers in a constraint 10455753096412511862784
Number of bits of the biggest sum of numbers74
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1245.77
Number of variables21975
Total number of constraints25992
Number of constraints which are clauses4284
Number of constraints which are cardinality constraints (but not clauses)21707
Number of constraints which are nor clauses,nor cardinality constraints1
Minimum length of a constraint1
Maximum length of a constraint21975

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
minisat+5923ERR NOCERT 1203.47
Pueblo8261NS 0.315951
galena5435NS 0.495924
vallst_0.9.2589026NS 39.758
PBS46383NS 64.5342
sat4jpseudo7348SAT TO 1245.77
bsolo4959UNKNOWN 8.24275
pb2sat+zchaff10208UNKNOWN EXCODE 129.451