Skip to main content
SpringerLink
Log in

Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition

  • Conference paper
Intelligent Computer Mathematics (CICM 2014)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 8543))

Included in the following conference series:

Abstract

Cylindrical algebraic decompositions (CADs) are a key tool for solving problems in real algebraic geometry and beyond. We recently presented a new CAD algorithm combining two advances: truth-table invariance, making the CAD invariant with respect to the truth of logical formulae rather than the signs of polynomials; and CAD construction by regular chains technology, where first a complex decomposition is constructed by refining a tree incrementally by constraint. We here consider how best to formulate problems for input to this algorithm. We focus on a choice (not relevant for other CAD algorithms) about the order in which constraints are presented. We develop new heuristics to help make this choice and thus allow the best use of the algorithm in practice. We also consider other choices of problem formulation for CAD, as discussed in CICM 2013, revisiting these in the context of the new algorithm.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Arnon, D., Collins, G.E., McCallum, S.: Cylindrical algebraic decomposition I: The basic algorithm. SIAM J. Comput. 13, 865–877 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  2. Arnon, D.S., Mignotte, M.: On mechanical quantifier elimination for elementary algebra and geometry. J. Symb. Comp. 5(1-2), 237–259 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bradford, R., Chen, C., Davenport, J.H., England, M., Moreno Maza, M., Wilson, D.: Truth table invariant cylindrical algebraic decomposition by regular chains (submitted, 2014), Preprint: http://opus.bath.ac.uk/38344/

  4. Bradford, R., Davenport, J.H., England, M., McCallum, S., Wilson, D.: Cylindrical algebraic decompositions for boolean combinations. In: Proc. ISSAC 2013, pp. 125–132. ACM (2013)

    Google Scholar 

  5. Bradford, R., Davenport, J.H., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition (submitted, 2014), Preprint: http://opus.bath.ac.uk/38146/

  6. Bradford, R., Davenport, J.H., England, M., Wilson, D.: Optimising problem formulation for cylindrical algebraic decomposition. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 19–34. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  7. Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proc. ISSAC 2007, pp. 54–60. ACM (2007)

    Google Scholar 

  8. Brown, C.W., El Kahoui, M., Novotni, D., Weber, A.: Algorithmic methods for investigating equilibria in epidemic modelling. J. Symbolic Computation 41, 1157–1173 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  9. Chen, C., Moreno Maza, M.: An incremental algorithm for computing cylindrical algebraic decompositions. In: Proc. ASCM 2012. Springer (2012) (to appear), Preprint: arXiv:1210.5543v1

    Google Scholar 

  10. Chen, C., Moreno Maza, M., Xia, B., Yang, L.: Computing cylindrical algebraic decomposition via triangular decomposition. In: Proc. ISSAC 2009, pp. 95–102. ACM (2009)

    Google Scholar 

  11. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)

    Google Scholar 

  12. Collins, G.E.: Quantifier elimination by cylindrical algebraic decomposition – 20 years of progress. In: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts & Monographs in Symbolic Computation, pp. 8–23. Springer (1998)

    Google Scholar 

  13. Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comp. 12, 299–328 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  14. Davenport, J.H., Bradford, R., England, M., Wilson, D.: Program verification in the presence of complex numbers, functions with branch cuts etc. In: Proc. SYNASC 2012, pp. 83–88. IEEE (2012)

    Google Scholar 

  15. Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proc. ISSAC 2004, pp. 111–118. ACM (2004)

    Google Scholar 

  16. England, M., Bradford, R., Davenport, J.H., Wilson, D.: Understanding Branch Cuts of Expressions. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 136–151. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  17. England, M.: An implementation of CAD in Maple utilising problem formulation, equational constraints and truth-table invariance. Uni. Bath, Dept. Comp. Sci. Tech. Report Series, 2013-04 (2013), http://opus.bath.ac.uk/35636/

  18. Fotiou, I.A., Parrilo, P.A., Morari, M.: Nonlinear parametric optimization using cylindrical algebraic decomposition. In: Proc. CDC-ECC 2005, pp. 3735–3740 (2005)

    Google Scholar 

  19. Iwane, H., Yanami, H., Anai, H., Yokoyama, K.: An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination. In: Proc. SNC 2009, pp. 55–64 (2009)

    Google Scholar 

  20. Kahan, W.: Problem #9: an ellipse problem. SIGSAM Bull. 9(3), 11–12 (1975)

    Article  Google Scholar 

  21. McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proc. ISSAC 1999, pp. 145–149. ACM (1999)

    Google Scholar 

  22. Paulson, L.C.: MetiTarski: Past and future. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 1–10. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  23. Schwartz, J.T., Sharir, M.: On the “Piano-Movers” Problem: II. General techniques for computing topological properties of real algebraic manifolds. Adv. Appl. Math. 4, 298–351 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  24. Strzeboński, A.: Cylindrical algebraic decomposition using validated numerics. J. Symb. Comp. 41(9), 1021–1038 (2006)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Bath, Bath, BA2 7AY, U.K.

    Matthew England, Russell Bradford, James H. Davenport & David Wilson

  2. Chongqing Key Laboratory of Automated Reasoning and Cognition, Chongqing Institute of Green and Intelligent Technology, CAS, Chongqing, 400714, China

    Changbo Chen

  3. University of Western Ontario, London, N6A 5B7, Canada

    Marc Moreno Maza

Authors
  1. Matthew England
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Russell Bradford
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Changbo Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. James H. Davenport
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Marc Moreno Maza
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. David Wilson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, The University of Western Ontario, MC 375,, N6A 5B7, London, ON, Canada

    Stephen M. Watt

  2. Departments of Computer Science and Mathematical Sciences, University of Bath, Claverton Down, BA2 7AY, Bath, UK

    James H. Davenport

  3. School of Computer Science, Edgbaston, University of Birmingham, B15 2TT, Birmingham, UK

    Alan P. Sexton

  4. Faculty of Informatics, Masaryk University, Botanicá 6a, 60200, Brno, Czech Republic

    Petr Sojka

  5. Institute for Computing Sciences, Radboud University Nijmegen, Postbus 9010,, 6525, Nijmegen, GL, The Netherlands

    Josef Urban

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

England, M., Bradford, R., Chen, C., Davenport, J.H., Maza, M.M., Wilson, D. (2014). Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds) Intelligent Computer Mathematics. CICM 2014. Lecture Notes in Computer Science(), vol 8543. Springer, Cham. https://doi.org/10.1007/978-3-319-08434-3_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08434-3_5

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08433-6

  • Online ISBN: 978-3-319-08434-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation