Subdivision Strategies for Boxes in Branch-and-Bound Nonlinear Solvers and Verification

Most verified solvers for nonlinear interval systems of equations comprise two strategies: a branch-and-bound-type “location” phase for excluding regions that cannot contain a solution, and a “verification” phase for proving that the remaining regions do indeed contain solutions. In the first phase, subdivision is crucial for the efficiency of the solvers. We discuss several ways for subdivision and present robust strategies that are suited for a variety of nonlinear systems. Particular focus is on the choice of subdivision directions, subdivision points and the handling of unbounded intervals. Furthermore we discuss a method to discard parts of a box within subdivision. Numerical evaluations are given based on the nonlinear interval solver SONIC. In the verification phase, further subdivision can increase the strength of the verification tests. In this paper, we address methods for the rigorous implementation of symmetrical subdivision which is needed, e.g., in existence tests based on Borsuk’s theorem.