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

Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller

Research output: Contribution to journalArticlepeer-review

11 Downloads (Pure)

Abstract

ksmt is a CDCL-style calculus for solving non-linear constraints over the real numbers involving polynomials and transcendental functions. In this article we investigate properties of the ksmt calculus and show that it is a δ-complete decision procedure for bounded problems. For that purpose we provide concrete algorithms computing linearisations based on either uniform or local moduli of continuity of non-linear functions. The latter method is called local linearisation and is shown to have desirable properties sufficient for termination and which also allow for more efficient treatment of non-linear constraints. Our methods for constructing linearisations are based on computable analysis, in particular we introduce the Cauchy-compatible compact representation of reals and prove its names to be locally compact, allowing for more efficient computation of local linearisations while maintaining δ-completeness.
Original languageEnglish
Article number114125
Number of pages16
JournalTheoretical Computer Science
Volume975
Early online date16 Aug 2023
DOIs
Publication statusPublished - 9 Oct 2023

Keywords

  • non-linear constraints
  • SMT
  • computable analysis
  • linearization

Fingerprint

Dive into the research topics of 'The ksmt calculus is a δ-complete decision procedure for non-linear constraints'. Together they form a unique fingerprint.

Cite this