Result page for benchmark submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cmb.opb

Jump to solvers results

General information on the benchmark

Namesubmitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cmb.opb
MD5SUMa8596c98551f801a6658f1ce91b33278
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1053
Optimality of the best value was proved YES
Number of terms in the objective function 304
Biggest coefficient in the objective function 61
Number of bits for the biggest coefficient in the objective function 6
Sum of the numbers in the objective function 12887
Number of bits of the sum of numbers in the objective function 14
Biggest number in a constraint 61
Number of bits of the biggest number in a constraint 6
Biggest sum of numbers in a constraint 12887
Number of bits of the biggest sum of numbers14
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark63.6713
Number of variables304
Total number of constraints671
Number of constraints which are clauses671
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint28

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
bsolo265OPT 63.6713
galena1967SAT 1.11683
Pueblo7814SAT 1189.01
pb2sat+zchaff9787SAT TO 1210.57
sat4jpseudo3214SAT TO 1260.3
PBS42419UNKNOWN TO 1202.65
vallst_0.9.2583546UNKNOWN TO 1204.52
minisat+2210UNKNOWN TO 1208.94