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_27: Abstract A global optimization algorithm for nonconvex Generalized Disjunctive Programming (GDP) problems is proposed in this paper. By making use of convex underestimating functions for bilinear, linear fractional and concave separable functions in the continuous variables, the convex hull of each nonlinear disjunction is constructed. The relaxed convex GDP problem is then solved in the first level of a two-level branch and bound algorithm, in which a discrete branch and bound search is performed on the disjunctions to predict lower bounds. In the second level, a spatial branch and bound method is used to solve nonconvex NLP problems for updating the upper bound. The proposed algorithm exploits the convex hull relaxation for the discrete search, and the fact that the spatial branch and bound is restricted to fixed discrete variables in order to predict tight lower bounds. Application of the proposed algorithm to several example problems is shown, as well as a comparison with other algorithms.
  @cite_26: Introduction 1. Convex Analysis 2. Fundamentals of Nonlinear Operations 3. Duality Theory 4. Mixed-Integer Linear Optimization 5. Mixed-Integer Nonlinear Optimization 6. Process Synthesis 7. Heat Exchanger Network Synthesis 8. Distillation-Based Separation Systems Synthesis 9. Synthesis of Reactor Networks and Reactor-Separator-Recycle Systems
  @cite_22: This paper addresses the synthesis of distillation column configurations to separate non-azeotropic multicomponent mixtures containing N components. It is shown that, for sharp separations of an N-component mixture, it is possible to develop a superstructure that takes into account all of the possibilities, from thermally linked systems with only one reboiler and one condenser to sequences with only conventional columns [2(N − 1) condensers and reboilers]. All of the partially thermally linked superstructures are included. The superstructure is systematically generated using the state task network (STN) formalism, in which only the tasks that can be performed are specified, but not equipment. A set of logical relationships between tasks is proposed that allows only feasible configurations that use the minimum number of column sections and that takes into account the fact that the minimum number of column sections and the number of heat exchangers are not independent. The superstructure is modeled using ge...
  @cite_17: In this paper, we address the problem of optimal synthesis of an integrated water system, where water using processes and water treatment operations are combined into a single network such that the total cost of obtaining freshwater for use in the water using operations, and treating wastewater is globally minimized. A superstructure that incorporates all feasible design alternatives for water treatment, reuse and recycle, is proposed. We formulate the optimization of this structure as a non-convex Non-Linear Programming (NLP) problem, which is solved to global optimality. The problem takes the form of a non-convex Generalized Disjunctive Program (GDP) if there is a flexibility of choosing different treatment technologies for the removal of the various contaminants in the wastewater streams. A new deterministic spatial branch and contract algorithm is proposed for optimizing such systems, in which piecewise under- and over-estimators are used to approximate the non-convex terms in the original model to obtain a convex relaxation whose solution gives a lower bound on the global optimum. These lower bounds are made to converge to the solution within a branch and bound procedure. Several examples are presented to illustrate the optimization of the integrated networks using the proposed algorithm.
summary: We already discussed related work in the area of SMT solving and will therefore focus here on related work in optimization. Optimization problems with logical formulae frequently arise in practice; examples in process systems engineering include: choosing between multiple possible treatment technologies in a waste water treatment plant @cite_17 and designing distillation column configurations @cite_22 . Typically used techniques in process engineering will first translate logical rules into mathematical constraints (e.g., as detailed in @cite_26 ) and then solve the resulting MINLP problem; this process of formulating a mathematical optimization problem based on logical constraints and then transforming the resulting problem into a MINLP problem is known as Generalized Disjunctive Programming (GDP) @cite_27 . Our proposed method of solving MINLP using SMT technology is therefore complementary to GDP; GDP is an excellent formulation technology, but transforming to a MINLP problem and then using traditional optimization methods eliminates the possibility of directly exploiting logical constraints in the original formulation.