Using an SMT solver and Craig interpolation to detect and remove redundant linear constraints in representations of non-convex polyhedra
Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid · 2008
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 solver and then removes the redundant constraints based on Craig interpolation. The approach is evaluated both for formulas from the model checking context including boolean combinations of linear constraints and boolean variables and for random trees composed of quantifiers, AND-, OR-, NOT-operators, and linear constraints produced by a generator. The results clearly show the advantages of our approach in comparison to state-of-the-art solvers.