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

arXiv: https://arxiv.org/abs/1905.09227 · HTML: https://mlsanity.com/paper/1905.09227/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 May 2019.

## Built on by (most cited first, 3 of 3)

- [Bayesian Optimisation with Formal Guarantees](https://mlsanity.com/paper/2106.06067/) (2021)
- [Proof Generation in CDSAT](https://mlsanity.com/paper/2107.02351/) (2021)
- [SMLP: Symbolic Machine Learning Prover](https://mlsanity.com/paper/2402.01415/) (2024)

## Abstract (arXiv)

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.