solver-z: rewrite runtime solver selection

Previously, only the exhaustive solver was used and could lead to NOEM.
This patch allows to switches from B&B solver, exhaustive solver and a
local greedy solver according to the complexity of the constraint.

(Reference: #35).
1 job for master in 1 minute and 26 seconds