Name
Title | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-00768-2_32 | TACAS |
Keywords | Field | DocType |
linear constraint,craig interpolation,arbitrary boolean combination,so-called redundant linear constraint,non-convex polyhedra,optimization method,satisfiability modulo theories,redundant constraint,redundant linear constraints,linear arithmetic,boolean variable,linear hybrid automata,computing optimized representations,quantifier elimination,model checking | Quantifier elimination,Discrete mathematics,Model checking,Computer science,Polyhedron,Algorithm,Regular polygon,Theoretical computer science,Solver,Boolean data type,Satisfiability modulo theories,Craig interpolation | Conference |
Volume | ISSN | Citations |
5505 | 0302-9743 | 14 |
PageRank | References | Authors |
1.31 | 20 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christoph Scholl | 1 | 346 | 32.07 |
| Stefan Disch | 2 | 87 | 6.37 |
| Florian Pigorsch | 3 | 140 | 9.21 |
| Stefan Kupferschmid | 4 | 72 | 7.05 |