Result page for benchmark submitted/manquinho/logic-synthesis/normalized-rot.b.opb

Jump to solvers results

General information on the benchmark

Namesubmitted/manquinho/logic-synthesis/normalized-rot.b.opb
MD5SUMc5ca4962151c0e84eeae44e16faee495
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 118
Optimality of the best value was proved NO
Number of terms in the objective function 1452
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 1452
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1452
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.38
Number of variables1451
Total number of constraints2984
Number of constraints which are clauses2932
Number of constraints which are cardinality constraints (but not clauses)52
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint81

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
minisat+915ERR NOCERT 1207.19
galena722SAT 1.08283
Pueblo7681SAT 1189.02
bsolo157SAT 1195.38
pb2sat+zchaff9592SAT TO 1204.79
sat4jpseudo1170SAT TO 1254.31
vallst_0.9.2581281UNKNOWN TO 1201.17
PBS41106UNKNOWN TO 1206.72