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

Jump to solvers results

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-core2536-691.opb
MD5SUM127ff6a7c180d4ca2c922cfd5e8d4802
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 939008000000000
Optimality of the best value was proved NO
Number of terms in the objective function 15554
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 215744503004511174656
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 10455744503004511862784
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 benchmark1203.88
Number of variables15554
Total number of constraints17823
Number of constraints which are clauses2536
Number of constraints which are cardinality constraints (but not clauses)15286
Number of constraints which are nor clauses,nor cardinality constraints1
Minimum length of a constraint1
Maximum length of a constraint15554

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
minisat+5958ERR NOCERT 1132.51
Pueblo8285NS 0.235963
galena5459NS 0.357944
vallst_0.9.2589049NS 21.8867
PBS46403NS 34.3248
sat4jpseudo7390SAT TO 1203.88
bsolo4982UNKNOWN 5.62814
pb2sat+zchaff10244UNKNOWN EXCODE 124.922