2021/04/27 by Franz Brauße, Konstantin Korovin, Brauße, Franz +5
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO
paper · pdf · doi:10.48550/arxiv.2104.13269
The conference version of this paper is accepted at CADE-28
arxiv created 2021/04/27 · arxiv updated 2021/04/28
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.