Solving non-linear constraints in CDCL style.

Konstatin Korovin

We will discuss a new conflict-driven method for solving non-linear constraints, called ksmt. Our approach is in the spirit of conflict resolution for linear arithmetic and related model-based methods such as NLSAT and MCSAT. To deal with non-linear components we numerically construct restricted linearisations using methods from computable analysis. Our approach covers a large number non-linear real functions including polynomials, exponentials, trigonometric and some discontinuous functions.