# A CDCL-style calculus for solving non-linear constraints

## TL;DR

This paper introduces ksmt, a novel CDCL-style calculus for checking the satisfiability of non-linear real constraints, combining symbolic and numerical methods with restricted linearizations, effective on various non-linear functions.

## Contribution

It presents a new conflict-driven calculus for non-linear SMT solving that integrates symbolic and numerical techniques with restricted linearizations.

## Key findings

- Effective on a wide range of non-linear functions
- Compared favorably with state-of-the-art SMT solvers
- Prototypical implementation demonstrates practical viability

## Abstract

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.