We present a method for exact global nonlinear optimization based on a real algebraic adaptation of the conflict-driven clause learning (CDCL) approach of modern SAT solving. This method allows polynomial objective functions to be constrained by real algebraic constraint systems with arbitrary boolean structure. Moreover, it can correctly determine when an objective function is unbounded, and can compute exact infima and suprema when they exist. The method requires computations over real closed fields containing infinitesimals (cf. ).
Joint work with Leonardo de Moura of Microsoft Research, Redmond.
1. Leonardo de Moura and Grant Olney Passmore. Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals.
In Proceedings of the 24th International Conference on Automated Deduction (CADE) (2013)