AbstractCylindrical Algebraic Decomposition was first introduced by Collins in 1975, to help understand and analyse the real algebraic geometry of a system of polynomials. There are various applications of CAD, specifically quantifier elimination problems in fields ranging from motion planning to analysing financial markets.
CAD algorithms are extremely useful for solving a system of polynomials, but the complexity of CAD algorithms is doubly exponential in the number of variables. This makes it difficult to use for large examples. McCallum attempted to tackle this problem first by switching from sign invariant CADs to order invariant CADs and then by exploiting equational constraints in the input formulae.
However, with the switch to order invariance, if the input formulae contain polynomial constraints that nullify over a region, the CAD algorithms produce an error. Lazard formulated a theory using the lex-least valuation, which removed the nullification problem for general CADs.
In this thesis we carry forward Lazard’s theory to exploit equational constraints and tackle the doubly exponential complexity of CAD algorithms. To do this we study the geometry of loci where nullification occurs, which we call curtains. Further to this we adapt our modifications to the most recent algorithm proposed by Brown- McCallum in 2020. We end with a comparison of the theoretical complexity of all the modifications presented in this thesis.
|Date of Award
|17 Nov 2021
|James Davenport (Supervisor) & Gregory Sankaran (Supervisor)
- Cylindrical Algebraic Decomposition