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

Jump to solvers results

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-sp97ic.opb
MD5SUMe8862b41c9b4f49ec8d11d1df0495e74
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 6288114893
Optimality of the best value was proved NO
Number of terms in the objective function 12497
Biggest coefficient in the objective function 1010107916
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 3093137085579
Number of bits of the sum of numbers in the objective function 42
Biggest number in a constraint 1010107916
Number of bits of the biggest number in a constraint 30
Biggest sum of numbers in a constraint 3093137085579
Number of bits of the biggest sum of numbers42
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1242.78
Number of variables12497
Total number of constraints13530
Number of constraints which are clauses41
Number of constraints which are cardinality constraints (but not clauses)13312
Number of constraints which are nor clauses,nor cardinality constraints177
Minimum length of a constraint1
Maximum length of a constraint6739

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
Pueblo8275NS 4.20536
galena5451NS 8.48871
vallst_0.9.2589039NS 18.0832
PBS46436NS 1209.44
bsolo5015SAT 1195.37
sat4jpseudo7376SAT TO 1242.78
pb2sat+zchaff10226UNKNOWN EXCODE 120.849
minisat+5946UNKNOWN TO 1207.79