SAT-Based Branch Bound and Optimal Control of Hybrid Dynamical Systems

摘要

A classical hybrid MIP-CSP approach for solving problems having a logical part and a mixed integer programming part is presented. A Branch and Bound procedure combines an MIP and a SAT solver to determine the optimal solution of a general class of optimization problems. The procedure explores the search tree, by solving at each node a linear relaxation and a satisfiability problem, until all integer variables of the linear relaxation are set to an integer value in the optimal solution. When all integer variables are fixed the procedure switches to the SAT solver which tries to extend the solution talcing into account logical constraints. If this is impossible, a "no-good" cut is generated and added to the linear relaxation. We show that the class of problems we consider turns out to be very useful for solving complex optimal control problems for linear hybrid dynamical systems formulated in discrete-time. We describe how to model the "hybrid" dynamics so that the optimal control problem can be solved by the hybrid MIP+SAT solver, and show that the achieved performance is superior to the one achieved by commercial MIP solvers.