Back to Search Start Over

Constructing a single cell in cylindrical algebraic decomposition

Authors :
Christopher W. Brown
Marek Košta
United States Naval Academy
Modeling and Verification of Distributed Algorithms and Systems (VERIDIS)
Max-Planck-Institut für Informatik (MPII)
Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est
Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM)
Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA)
Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA)
Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)
The second author is supported by the German Transregional Collaborative Research Center SFB/TR 14 AVACS.
Department of Formal Methods (LORIA - FM)
Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est
Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII)
Max-Planck-Gesellschaft-Max-Planck-Gesellschaft
Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA)
Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)
Source :
Journal of Symbolic Computation, Journal of Symbolic Computation, Elsevier, 2014, pp.35. ⟨10.1016/j.jsc.2014.09.024⟩, Journal of Symbolic Computation, 2014, pp.35. ⟨10.1016/j.jsc.2014.09.024⟩
Publication Year :
2014
Publisher :
HAL CCSD, 2014.

Abstract

International audience; 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.

Details

Language :
English
ISSN :
07477171 and 1095855X
Database :
OpenAIRE
Journal :
Journal of Symbolic Computation, Journal of Symbolic Computation, Elsevier, 2014, pp.35. ⟨10.1016/j.jsc.2014.09.024⟩, Journal of Symbolic Computation, 2014, pp.35. ⟨10.1016/j.jsc.2014.09.024⟩
Accession number :
edsair.doi.dedup.....144fb38b71a98c5cee4f7340ce4a2ae4
Full Text :
https://doi.org/10.1016/j.jsc.2014.09.024