Certified Numerical Real Root Isolation of Zero-dimensional Multivariate Real Nonlinear Systems

Using the local geometrical properties of a given zero-dimensional square multivariate nonlinear system inside a box, we provide a simple but effective and new criterion for the uniqueness and the existence of a real simple zero of the system inside the box. Based on the result, we design an algorithm based on subdivision and interval arithmetics to isolate all the real zeros of a general real nonlinear system inside a given box. Our method is complete for systems with only finite isolated simple real zeros inside a box. A termination precision is given for general zero-dimensional systems. Multiple zeros of the system are output in bounded boxes. A variety of benchmarks show the effectivity and efficiency of our implementation (in C++). It works for polynomial systems with Bezout bound more than 100 million. It also works for non-polynomial nonlinear systems. We also discuss the limitations of our method.