Simulation and Optimization by Quantifier Elimination

We present a highly optimized method for the elimination of linear variables from a Boolean combination of polynomial equations and inequalities. In contrast to the basic method described earlier, the practical applicability of the present method goes far beyond academic examples. The optimization is achieved by various strategies to prune superfluous branches in the elimination tree constructed by the method. The main application concerns the simulation of large technical networks of (electric, mechanical or hydraulic) components, whose characteristic curves are piecewise linear (or quadratic) in the variables to be eliminated. Typical goals are the computation of admissible ranges for certain variables and the detection of a malfunction of a network component. The algorithms are currently used in a commercial software system for industrial applications. Moreover, we extend the authorʹs elimination method for parametric linear programming to the non-convex case by allowing arbitrary combinations of parametric linear inequalities as constraints. We present a new strategy for finding smaller elimination sets and thus smaller elimination trees for parametric linear programming. Some benchmark examples from the library of problems show the significance of this strategy even for convex linear programming problems.