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

Jump to solvers results

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-core4872-1529.opb
MD5SUM21523a021e6bde8cb1bd98f2664add6c
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 2030592000000000
Optimality of the best value was proved NO
Number of terms in the objective function 24975
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 226603053881884901376
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 10466603053881885720576
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 benchmark1206.69
Number of variables24975
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 constraint24975

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
Pueblo8262NS 0.348946
galena5436NS 0.565913
vallst_0.9.2589027NS 45.1881
PBS46384NS 83.4163
sat4jpseudo7349SAT TO 1206.69
bsolo4960UNKNOWN 11.1743
pb2sat+zchaff10209UNKNOWN EXCODE 135.163
minisat+5922UNKNOWN TO 1207.92