Automated Reasoning For The Existence Of Darboux Polynomials

Given a polynomial ordinary differential equation (ODE), we devise generic polynomial reduction algorithms to automatically investigate the intertwined relationship between the total degree of (nontrivial) Darboux polynomials and the polynomials defining the ODE. By generic we mean that both the coefficients and the multidegree of the involved polynomials are symbolic. We use Newton polytopes as a light-weight abstraction to select optimal weight monomial orders improving the efficiency of the involved computations. The method works by inferring necessary conditions on both the coefficients and the multidegree for the polynomial to be Darboux. These conditions are then used, via constants' propagation, to restrict the shape of the generic candidate, pinpointing which monomials ought to be preserved by removing the superfluous ones. In some relevant cases, we are able to automatically prove the nonexistence of (nontrivial) Darboux polynomials providing a new toolbox to prove and formally certify that some limit cycles are not algebraic.