# The ksmt calculus is a δ-complete decision procedure for non-linear constraints

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Apr 2021.

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

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

## Abstract (arXiv)

ksmt is a CDCL-style calculus for solving non-linear constraints over real numbers involving polynomials and transcendental functions. In this paper we investigate properties of the ksmt calculus and show that it is a δ-complete decision procedure for bounded problems. We also propose an extension with local linearisations, which allow for more efficient treatment of non-linear constraints.