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

Jump to solvers results

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-CMS750_4.opb
MD5SUM7cb58e3aea22e107ecbc4e74969c24f1
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 877568
Optimality of the best value was proved NO
Number of terms in the objective function 780
Biggest coefficient in the objective function 536870912
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 1074509823
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 1024000000
Number of bits of the biggest number in a constraint 30
Biggest sum of numbers in a constraint 2147731454
Number of bits of the biggest sum of numbers32
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark
Number of variables142226
Total number of constraints28077
Number of constraints which are clauses2438
Number of constraints which are cardinality constraints (but not clauses)7196
Number of constraints which are nor clauses,nor cardinality constraints18443
Minimum length of a constraint1
Maximum length of a constraint61

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
galena5450NS 31.6262
vallst_0.9.2589086NS 441.982
Pueblo8443NS 1189.39
PBS46425NS 1202.98
sat4jpseudo7350SAT TO 1267.57
bsolo5001UNKNOWN 1196.69
pb2sat+zchaff10320UNKNOWN MO 899.261
minisat+5924UNKNOWN TO 1205.43