Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints

Abstract. We present a method which computes optimized representations for non-convex polyhedra. Our method detects so-called redundant linear constraints in these representations by using an incremental SMT (Satisfiability Modulo Theories) solver and then removes the redundant constraints based on Craig interpolation. The approach is motivated by applications in the context of model checking for Linear Hybrid Automata. Basically, it can be seen as an optimization method for formulas including arbitrary boolean combinations of linear constraints and boolean variables. We show that our method provides an essential step making quantifier elimination for linear arithmetic much more efficient. Experimental results clearly show the advantages of our approach in comparison to state-of-the-art solvers.

• Type: Conference
• Year: 2009
• Where: TACAS
• Authors: Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid
• Keywords: Linear Constraints, Redundant Constraints, Redundant Linear Constraints, TACAS 2009