2019/05/22 by Franz Brauße, Konstantin Korovin, Brauße, Franz +5 · 1 citation
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO
paper · pdf · doi:10.48550/arxiv.1905.09227
17 pages, 3 figures; accepted at FroCoS 2019; software available at <http://informatik.uni-trier.de/~brausse/ksmt/>
arxiv created 2019/07/05 · arxiv updated 2019/07/08
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.