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

Jump to solvers results

General information on the benchmark

Namesubmitted/manquinho/logic-synthesis/normalized-9sym.b.opb
MD5SUM1457dc2646bff5e87c0f4b32dfb926ba
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 5
Optimality of the best value was proved YES
Number of terms in the objective function 310
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 310
Number of bits of the sum of numbers in the objective function 9
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 310
Number of bits of the biggest sum of numbers9
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark0.734888
Number of variables309
Total number of constraints976
Number of constraints which are clauses963
Number of constraints which are cardinality constraints (but not clauses)13
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint87

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
galena711OPT 0.734888
minisat+811OPT 1.25781
pb2sat+zchaff9499OPT 26.007
Pueblo7614OPT 79.7489
vallst_0.9.2581210OPT 174.5
bsolo68OPT 332.867
sat4jpseudo1112OPT 377.06
PBS41084OPT 910.329