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

Jump to solvers results

General information on the benchmark

Namesubmitted/manquinho/synthesis-ptl-cmos-circuits/normalized-C432.opb
MD5SUM6292e63147fb202dc159fbf5a9ff5c77
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 4882
Optimality of the best value was proved NO
Number of terms in the objective function 771
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 33355
Number of bits of the sum of numbers in the objective function 16
Biggest number in a constraint 61
Number of bits of the biggest number in a constraint 6
Biggest sum of numbers in a constraint 33355
Number of bits of the biggest sum of numbers16
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1196.31
Number of variables771
Total number of constraints1951
Number of constraints which are clauses1949
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints2
Minimum length of a constraint1
Maximum length of a constraint42

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
minisat+2199ERR NOCERT 1208.22
galena1963SAT 1.04984
Pueblo7797SAT 1189.01
bsolo317SAT 1196.31
sat4jpseudo3195SAT TO 1256.59
pb2sat+zchaff9700UNKNOWN EXCODE 320.662
vallst_0.9.2583496UNKNOWN TO 1200.89
PBS42407UNKNOWN TO 1200.95