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

Jump to solvers results

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-core2586-950.opb
MD5SUMc9d9583d3d7a74a0edfae6842f5e5cad
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1258496000000000
Optimality of the best value was proved NO
Number of terms in the objective function 13545
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 226583943993884901376
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 10466583943993884672000
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 benchmark1239.85
Number of variables13545
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 constraint13545

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
minisat+5921ERR NOCERT 1084.78
Pueblo8260NS 0.194969
galena5430NS 0.309952
vallst_0.9.2589025NS 17.6143
PBS46380NS 23.5804
sat4jpseudo7347SAT TO 1239.85
bsolo4958UNKNOWN 4.94025
pb2sat+zchaff10207UNKNOWN EXCODE 122.212