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

Jump to solvers results

General information on the benchmark

Namemps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-core2586-950.opb
MD5SUMd227b04d1ac4226bb8116c410fa055ae
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 157824000000000
Optimality of the best value was proved NO
Number of terms in the objective function 13435
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 224301741012582900
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 1280224301741012680704
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 benchmark1207.46
Number of variables13435
Total number of constraints15804
Number of constraints which are clauses2586
Number of constraints which are cardinality constraints (but not clauses)13217
Number of constraints which are nor clauses,nor cardinality constraints1
Minimum length of a constraint1
Maximum length of a constraint13435

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
minisat+6323ERR NOCERT 1202.92
Pueblo8645NS 0.202968
galena5816NS 0.308952
vallst_0.9.2589409NS 17.4124
PBS46830NS 1207.31
sat4jpseudo8962SAT TO 1207.46
bsolo5344UNKNOWN 20.3579
pb2sat+zchaff10593UNKNOWN EXCODE 124.127