text: 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.
  @cite_7: The Branch-And-Reduce Optimization Navigator (BARON) is a computational system for facilitating the solution of nonconvex optimization problems to global optimality. We provide a brief description of the algorithms used by the software, describe the types of problems that can be currently solved and summarize our recent computational experience. BARON is available by anonymous ftp from aristotle. me. uiuc. edu.
  @cite_8: The global solver in the LINDO Application Programming Interface (LINDO API) finds guaranteed global optima to nonconvex, nonlinear and integer mathematical models using the branch and bound relax approach. We describe (a) the class of problems for which it tends to be appropriate; (b) how to access it directly via the LINDO API or via various modelling language front ends; (c) heuristics used for finding good initial solutions; (d) methods for constructing easily solved relaxations; (e) branching rules for splitting a problem into more easily solved subproblems; and (f) some illustrative computational results.
  @cite_24: This article introduces constraint integer programming (CIP), which is a novel way to combine constraint programming (CP) and mixed integer programming (MIP) methodologies. CIP is a generalization of MIP that supports the notion of general constraints as in CP. This approach is supported by the CIP framework SCIP, which also integrates techniques from SAT solving. SCIP is available in source code and free for non-commercial use. We demonstrate the usefulness of CIP on two tasks. First, we apply the constraint integer programming approach to pure mixed integer programs. Computational experiments show that SCIP is almost competitive to current state-of-the-art commercial MIP solvers. Second, we employ the CIP framework to solve chip design verification problems, which involve some highly non-linear constraint types that are very hard to handle by pure MIP solvers. The CIP approach is very effective here: it can apply the full sophisticated MIP machinery to the linear part of the problem, while dealing with the non-linear constraints by employing constraint programming techniques.
  @cite_31: Many industrial problems can be naturally formulated using mixed integer non-linear programming (MINLP) models and can be solved by spatial Branch&Bound (sBB) techniques. We study the impact of two important parts of sBB methods: bounds tightening (BT) and branching strategies. We extend a branching technique originally developed for MILP, reliability branching, to the MINLP case. Motivated by the demand for open-source solvers for real-world MINLP problems, we have developed an sBB software package named couenne (Convex Over-and Under-ENvelopes for Non-linear Estimation) and used it for extensive tests on several combinations of BT and branching techniques on a set of publicly available and real-world MINLP instances. We also compare the performance of couenne with a state-of-the-art MINLP solver.
  @cite_16: This manuscript introduces ANTIGONE, Algorithms for coNTinuous Integer Global Optimization of Nonlinear Equations, a general mixed-integer nonlinear global optimization framework. ANTIGONE is the evolution of the Global Mixed-Integer Quadratic Optimizer, GloMIQO, to general nonconvex terms. The purpose of this paper is to show how the extensible structure of ANTIGONE realizes our previously-proposed mixed-integer quadratically-constrained quadratic program and mixed-integer signomial optimization computational frameworks. To demonstrate the capacity of ANTIGONE, this paper presents computational results on a test suite of @math 2 , 571 problems from standard libraries and the open literature; we compare ANTIGONE to other state-of-the-art global optimization solvers.
summary: With respect to MINLP solvers based on traditional branch-and-bound approaches @cite_24 @cite_31 @cite_8 @cite_16 @cite_7 , the advantage of the overall approach taken in tool is that -- as in most SMT-based approaches -- there is support for incremental strategies such as push pop. Typical MINLP solvers will fathom, i.e. discard, regions of the tree as soon as they determine that this region cannot include the global solution.