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

Jump to solvers results

General information on the benchmark

Namemps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-core4872-1529.opb
MD5SUM7eea141e02c7a2753145fd63f1e9087d
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 253696000000000
Optimality of the best value was proved NO
Number of terms in the objective function 24865
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 226690477012582900
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 1280226690477012549632
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 benchmark1206.48
Number of variables24865
Total number of constraints29520
Number of constraints which are clauses4872
Number of constraints which are cardinality constraints (but not clauses)24647
Number of constraints which are nor clauses,nor cardinality constraints1
Minimum length of a constraint1
Maximum length of a constraint24865

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
Pueblo8648NS 0.344947
galena5821NS 0.567913
vallst_0.9.2589449NS 1203.67
PBS46845NS 1208.9
sat4jpseudo8970SAT TO 1206.48
bsolo5353UNKNOWN 74.7326
pb2sat+zchaff10597UNKNOWN EXCODE 131.976
minisat+6325UNKNOWN TO 1208.74