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

Jump to solvers results

General information on the benchmark

Namesubmitted/manquinho/logic-synthesis/normalized-alu4.b.opb
MD5SUMdb06e7fbd4f70a4af68f8f196fdb3636
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 50
Optimality of the best value was proved NO
Number of terms in the objective function 808
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 808
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 808
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.2
Number of variables807
Total number of constraints1838
Number of constraints which are clauses1823
Number of constraints which are cardinality constraints (but not clauses)15
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint98

Results of the different solvers on this benchmark

Solver NameTraceidAnswerCPU time
minisat+917ERR NOCERT 1209.18
galena724SAT 1.07783
Pueblo7641SAT 1189.02
bsolo161SAT 1195.2
pb2sat+zchaff9593SAT TO 1205.58
sat4jpseudo1188SAT TO 1267.45
PBS41109UNKNOWN TO 1200.53
vallst_0.9.2581286UNKNOWN TO 1202.85