cs.LO
A CDCL style calculus for solving non linear constraints. In this paper we propose a novel approach for checking satisfiability of non linear constraints over the reals, called ksmt. The procedure is based on conflict resolution in CDCL style calculus, using a composition of symbolical and numerical methods. To deal with the non linear components in case of conflicts we use numerically constructed restricted linearisations. This approach covers a large number of computable non linear real functions such as polynomials, rational or trigonometrical functions and beyond. A prototypical implementation has been evaluated on several non linear SMT LIB examples and the results have been compared with state of the art SMT solvers.