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

Jump to solvers results

General information on the benchmark

Namemps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-core2536-691.opb
MD5SUM1a2d760450612ad13ad0fc356acc93dc
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 117248000000000
Optimality of the best value was proved NO
Number of terms in the objective function 15464
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 214380061511534325
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 1280214380061511647232
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 benchmark1245.95
Number of variables15464
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 constraint15464

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
minisat+6349ERR NOCERT 1205.64
Pueblo8669NS 0.228964
galena5846NS 0.352945
vallst_0.9.2589437NS 21.8307
PBS47270NS 1209.65
sat4jpseudo9006SAT TO 1245.95
bsolo5367UNKNOWN 33.6109
pb2sat+zchaff10623UNKNOWN EXCODE 123.026