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

Jump to solvers results

General information on the benchmark

Namesubmitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cm42a.opb
MD5SUM62b75258091a8b1382fa8b1c633d9511
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 694
Optimality of the best value was proved YES
Number of terms in the objective function 99
Biggest coefficient in the objective function 60
Number of bits for the biggest coefficient in the objective function 6
Sum of the numbers in the objective function 4087
Number of bits of the sum of numbers in the objective function 12
Biggest number in a constraint 60
Number of bits of the biggest number in a constraint 6
Biggest sum of numbers in a constraint 4087
Number of bits of the biggest sum of numbers12
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark13.371
Number of variables99
Total number of constraints185
Number of constraints which are clauses185
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 constraint2
Maximum length of a constraint20

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
bsolo260OPT 13.371
galena1966SAT 1.19282
Pueblo7836SAT 1189
pb2sat+zchaff9786SAT TO 1208.58
sat4jpseudo3212SAT TO 1227.58
PBS42416UNKNOWN TO 1201.05
vallst_0.9.2583537UNKNOWN TO 1202.87
minisat+2203UNKNOWN TO 1209.84