Skip to main content
SpringerLink
Log in

Efficient Elimination of Redundancies in Polyhedra by Raytracing

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10145))

Abstract

A polyhedron can be represented as constraints, generators or both in the double description framework. Whatever the representation, most polyhedral operators spend a significant amount of time to maintain minimal representations. To minimize a polyhedron in constraints-only representation, the redundancy of each constraint must be checked with respect to others by solving a linear programming (lp) problem. We present an algorithm that replaces most lp problem resolutions by distance computations. It consists in launching rays starting from a point within the polyhedron and orthogonal to its bounding hyperplanes. A face first encountered by one of these rays is an irredundant constraint of the polyhedron. Since this procedure is incomplete, lp problem resolutions are required for the remaining undetermined constraints. Experiments show that our algorithm drastically reduces the number of calls to the simplex, resulting in a considerable speed improvement. To follow the geometric interpretation, the algorithm is explained in terms of constraints but it can also be used to minimize generators.

This work was partially supported by the European Research Council under the European Union’s Seventh Framework Programme (FP/2007-2013)/ERC Grant Agreement nr. 306595 “STATOR”.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We only deal with convex polyhedra. For readability, we will omit the adjective convex in the following.

  2. 2.

    Conversely, simplex \(\left( \exists \varvec{w}, \left\langle \varvec{\varvec{C_{}}'},\varvec{\varvec{w}}\right\rangle >0 \bigwedge _i \left\langle \varvec{\varvec{C_{i}}},\varvec{\varvec{w}}\right\rangle \le 0 \right) \) returns either \(\textsc {success} (\varvec{w})\) or \(\textsc {failure} (\varvec{\lambda })\) such that \( \varvec{C_{}}' = \sum _i \lambda _i \varvec{C_{i}}\).

  3. 3.

    As this property is a pure technicality it is not given here but is available in [15].

  4. 4.

    What is needed from the floating point solution is the set of basic variables and an ordering of the nonnull \(\lambda _i\) coefficients to speed up the search in exact simplex.

  5. 5.

    https://github.com/VERIMAG-Polyhedra.

  6. 6.

    The opposite phenomena (2n vertices corresponding to \(2^n\) constraints) also exists but hardly ever occurs in practice [3].

References

  1. Anderson, E., Bai, Z., Bischof, C., Blackford, S., Demmel, J., Dongarra, J., Croz, J., Greenbaum, A., Hammarling, S., McKenney, A., Sorensen, D.: LAPACK Users’ Guide, 3rd edn. Society for Industrial and Applied Mathematics, Philadelphia (1999)

    Book  MATH  Google Scholar 

  2. Bagnara, R., Hill, P.M., Zaffanella, E.: Applications of polyhedral computations to the analysis and verification of hardware and software systems. Theoret. Comput. Sci. 410(46), 4672–4691 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  3. Benoy, F., King, A., Mesnard, F.: Computing convex hulls with a linear solver. TPLP: Theory Pract. Log. Program. 5(1–2), 259–271 (2005)

    MATH  Google Scholar 

  4. Chernikova, N.V.: Algorithm for discovering the set of all the solutions of a linear programming problem. USSR Comput. Math. Math. Phys. 8, 282–293 (1968)

    Article  MATH  Google Scholar 

  5. Chvatal, V.: Linear Programming. Series of Books in the Mathematical Sciences. W. H. Freeman, New York (1983)

    MATH  Google Scholar 

  6. Feautrier, P., Lengauer, C.: Polyhedron model. In: Padua, D. (ed.) Encyclopedia of Parallel Computing, vol. 1, pp. 1581–1592. Springer, Berlin (2011)

    Google Scholar 

  7. Fouilhé, A., Monniaux, D., Périn, M.: Efficient certificate generation for the abstract domain of polyhedra. In: Static Analysis Symposium (2013)

    Google Scholar 

  8. Fukuda, K., Prodon, A.: Double description method revisited. In: Deza, M., Euler, R., Manoussakis, I. (eds.) CCS 1995. LNCS, vol. 1120, pp. 91–111. Springer, Heidelberg (1996). doi:10.1007/3-540-61576-8_77

    Chapter  Google Scholar 

  9. Goldman, A.J., Tucker, A.W.: Polyhedral convex cones. In: Kuhn, H.W., Tucker, A.W. (eds.) Linear Inequalities and Related Systems. Annals of Mathematics Studies, vol. 38, pp. 19–40. Princeton University Press, Princeton (1956)

    Google Scholar 

  10. Halbwachs, N.: Détermination automatique de relations linéaires vérifiées par les variables d’un programme. Ph.D. thesis, Université scientifique et médicale de Grenoble, (in French) (1979)

    Google Scholar 

  11. Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_52

    Chapter  Google Scholar 

  12. Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: ACM Principles of Programming Languages (POPL), pp. 247–259. ACM Press, January 2015

    Google Scholar 

  13. Lassez, J.-L., Huynh, T., McAloon, K.: Simplification and elimination of redundant linear arithmetic constraints. In: Constraint Logic Programming, pp. 73–87. MIT Press, Cambridge (1993)

    Google Scholar 

  14. Le Verge, H.: A note on Chernikova’s algorithm. Research report RR-1662, INRIA (1992)

    Google Scholar 

  15. Maréchal, A., Périn, M.: Efficient elimination of redundancies in polyhedra using raytracing. Technical report TR-2016-6, Verimag, Université Grenoble-Alpes, October 2016

    Google Scholar 

  16. Motzkin, T.S., Raiffa, H., Thompson, G.L., Thrall, R.M.: The double description method. In: Contributions to the Theory of Games. Annals of Mathematics Studies, vol. 2, pp. 51–73. Princeton University Press, Princeton (1953)

    Google Scholar 

  17. Schrijver, A.: Theory of Linear and Integer Programming. Wiley-Interscience Series in Discrete Mathematics and Optimization. Wiley, Hoboken (1999)

    MATH  Google Scholar 

  18. Simon, A., King, A.: Exploiting sparsity in polyhedral analysis. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 336–351. Springer, Heidelberg (2005). doi:10.1007/11547662_23

    Chapter  Google Scholar 

  19. Wilde, D.K.: A library for NG polyhedral operations. Master’s thesis, Oregon State University, Corvallis, Oregon, December 1993. Also Published as IRISA Technical report PI 785, Rennes, France (1993)

    Google Scholar 

  20. Zolotykh, N.Y.: New modification of the double description method for constructing the skeleton of a polyhedral cone. Comput. Math. Math. Phys. 52(1), 146–156 (2012)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université Grenoble-Alpes, VERIMAG, 38000, Grenoble, France

    Alexandre Maréchal & Michaël Périn

Authors
  1. Alexandre Maréchal
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michaël Périn
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexandre Maréchal .

Editor information

Editors and Affiliations

  1. IRIF, Université Paris Diderot, Paris, France

    Ahmed Bouajjani

  2. VERIMAG, CNRS & Université Grenoble Alpes, Grenoble, France

    David Monniaux

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Maréchal, A., Périn, M. (2017). Efficient Elimination of Redundancies in Polyhedra by Raytracing. In: Bouajjani, A., Monniaux, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2017. Lecture Notes in Computer Science(), vol 10145. Springer, Cham. https://doi.org/10.1007/978-3-319-52234-0_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-52234-0_20

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-52233-3

  • Online ISBN: 978-3-319-52234-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation