  Optimization of Mixed-Integer Non-Linear Programming (MINLP) supports
important decisions in applications such as Chemical Process Engineering. But
current solvers have limited ability for deductive reasoning or the use of
domain-specific theories, and the management of integrality constraints does
not yet exploit automated reasoning tools such as SMT solvers. This seems to
limit both scalability and reach of such tools in practice. We therefore
present a tool, ManyOpt, for MINLP optimization that enables experimentation
with reduction techniques which transform a MINLP problem to feasibility
checking realized by an SMT solver. ManyOpt is similar to the SAT solver
ManySAT in that it runs a specified number of such reduction techniques in
parallel to get the strongest result on a given MINLP problem. The tool is
implemented in layers, which we may see as features and where reduction
techniques are feature vectors. Some of these features are inspired by known
MINLP techniques whereas others are novel and specific to SMT. Our experimental
results on standard benchmarks demonstrate the benefits of this approach. The
tool supports a variety of SMT solvers and is easily extensible with new
features, courtesy of its layered structure. For example, logical formulas for
deductive reasoning are easily added to constrain further the optimization of a
MINLP problem of interest.
