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

Jump to solvers results

General information on the benchmark

Namemps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-core4284-1064.opb
MD5SUMa818b9a925b31116d60be3312981b83f
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 178432000000000
Optimality of the best value was proved NO
Number of terms in the objective function 21885
Biggest coefficient in the objective function 52428800000000000
Number of bits for the biggest coefficient in the objective function 56
Sum of the numbers in the objective function 215454237511534325
Number of bits of the sum of numbers in the objective function 58
Biggest number in a constraint 1280000000000000000000
Number of bits of the biggest number in a constraint 71
Biggest sum of numbers in a constraint 1280215454237511647232
Number of bits of the biggest sum of numbers71
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1202.77
Number of variables21885
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 constraint21885

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
minisat+6324ERR NOCERT 1201.62
Pueblo8647NS 0.31895
galena5820NS 0.499923
vallst_0.9.2589411NS 39.289
PBS46817NS 1209.08
sat4jpseudo8968SAT TO 1202.77
bsolo5348UNKNOWN 52.322
pb2sat+zchaff10595UNKNOWN EXCODE 129.354