Certified Complex Root Isolation via Adaptive Root Separation Bounds

We address the problem of {\em root isolation} for polynomial systems: for an affine, zero-dimensional polynomial system of $N$ equations in $N$ variables, we describe an algorithm to encapsulate all complex solutions into disjoint regions, each containing precisely one solution (called \emph{isolating regions}). Our approach also computes the multiplicity of each solution. The main novelty is a new approach to certify that a set of computed regions is indeed isolating. It is based on an adaptive root separation bound obtained from combining information about the approximate location of roots and resultant calculus. Here we use simple subdivision method to determine the number of roots within certain regions. The resultant calculus only takes place over prime fields to avoid the disadvantageous coefficient growth in symbolic methods, without sacrificing the exactness of the output. The presented approach is complete for uni- and bivariate systems, and in general applies in higher dimensions as well, possibly after a coordinate change