Note: This content is accessible to all versions of every browser. However, this browser does not seem to support current Web standards, preventing the display of our site's design details.


SMT Solvers for Embedded Hybrid MPC


M. Heinzmann

Semester Thesis; SS17

In this project we were interested in solving hybrid model predictive control (MPC) problems in which one aims at minimizing a quadratic cost function. For MPC to be practical, these problems have to be solved in milliseconds or even microseconds. From [4] we know that we can write hybrid MPC problems as mixed-integer quadratic programs (MIQP) subject to linear equalities and inequalities. However, MIQPs are known to be computationally demanding. Therefore solving these MPC problems within a short time poses a significant challenge. In this project we wanted to explore an alternative way to solve such problems. Namely we used satisfiability modulo theories (SMT) solvers. SMT solvers have often been used in the context of theorem-proving systems (such as PVS[13]) and extended static checking [9] where verification focuses on assertion checking. Our interests in this project were twofold. On the one hand, we wanted to find a general way how to formulate a hybrid MPC problem such that it can be solved by a SMT solver. On the other hand, we wanted to find out how todays state-of-the-art SMT solvers perform compared to MIQP solvers, with which one usually solves hybrid MPC problems with an underlying quadratic cost function. For that we simulated our generalized SMT formulation on two problems from the literature ([3] and [4]) and compared to results obtained from MIQP and SMT solvers.

Supervisors: Damian Frick, John Lygeros


Type of Publication:

(13)Semester/Bachelor Thesis

File Download:

Request a copy of this publication.
(Uses JavaScript)
% Autogenerated BibTeX entry
@PhdThesis { Xxx:2017:IFA_5658
Permanent link