The ksmt calculus is a $\delta$-complete decision procedure for non-linear constraints

TL;DR

This paper introduces the ksmt calculus, a decision procedure for non-linear real constraints, demonstrating its $elta$-completeness and proposing extensions for improved efficiency.

Contribution

The paper establishes the $elta$-completeness of ksmt calculus for bounded problems and proposes local linearizations to enhance its performance.

Findings

ksmt calculus is $elta$-complete for bounded non-linear problems

Extension with local linearizations improves efficiency

Demonstrates properties of the calculus in solving polynomial and transcendental constraints

Abstract

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 $\delta$-complete decision procedure for bounded problems. We also propose an extension with local linearisations, which allow for more efficient treatment of non-linear constraints.