HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Constructing a single cell in cylindrical algebraic decomposition

Christopher Brown 1 Marek Kosta 2
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : This paper presents an algorithm which, given a point and a set of polynomials, constructs a single cylindrical cell containing the point, such that the given polynomials are sign-invariant in the computed cell. To represent a single cylindrical cell, a novel data structure is introduced. The algorithm works with this representation and proceeds incrementally, i.e., first constructing a cell representing the whole real space, and then iterating over the input polynomials, refining the cell at each step to ensure the sign-invariance of the current input polynomial. A merge procedure realizing this refinement is described, and its correctness is proven. The merge procedure is based on McCallum's projection operator, but uses geometric information relative to the input point to reduce the number of projection polynomials computed. The use of McCallum's operator implies the incompleteness of the algorithm in general. However, the algorithm is complete for well-oriented sets of polynomials. Moreover, the incremental approach described in this paper can be easily adapted to a different projection operator. The cell construction algorithm presented in this paper is an alternative to the “model-based” method described by Jovanović and de Moura in a 2012 paper. It generalizes the algorithm described by the first author in a 2013 paper, which could only produce full-dimensional cells, to allow for the construction of cells of arbitrary dimension. While a thorough comparison, whether analytical or empirical, of the new algorithm and the “model-based” approach will be the subject of future work, this paper provides preliminary justification for asserting the superiority of the new method.
Document type :
Journal articles
Complete list of metadata

Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Friday, November 28, 2014 - 9:19:27 AM
Last modification on : Saturday, October 16, 2021 - 11:26:05 AM

Links full text




Christopher Brown, Marek Kosta. Constructing a single cell in cylindrical algebraic decomposition. Journal of Symbolic Computation, Elsevier, 2014, pp.35. ⟨10.1016/j.jsc.2014.09.024⟩. ⟨hal-01088452⟩



Record views