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

Jump to solvers results

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-berlin_5_8_0.opb
MD5SUM9a578fa18e88cebdbf227cdbb9fbab5f
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 64512
Optimality of the best value was proved NO
Number of terms in the objective function 78
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 1073790975
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 2147979262
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 variables9464
Total number of constraints2614
Number of constraints which are clauses309
Number of constraints which are cardinality constraints (but not clauses)794
Number of constraints which are nor clauses,nor cardinality constraints1511
Minimum length of a constraint1
Maximum length of a constraint61

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
minisat+5913ERR NOCERT 1208.13
galena5425NS 2.45263
Pueblo8436NS 1189.1
PBS46408NS 1201.63
vallst_0.9.2589087NS 1203.36
pb2sat+zchaff10335SAT TO 1202
sat4jpseudo7340SAT TO 1232.67
bsolo4480UNKNOWN 1195.51