A CDCL-Style Calculus for Solving Non-linear Constraints

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Authors:
  • Franz Brausse
  • Konstantin Korovin
  • Margarita Korovina
  • Norbert Mueller


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.

Bibliographical metadata

Original languageEnglish
Title of host publicationFrontiers of Combining Systems, 12th International Symposium
Subtitle of host publication FroCoS 2019, Proceedings
EditorsAndreas Herzig, Andrei Popescu
PublisherSpringer Nature
Pages 131-148
Number of pages18
ISBN (Electronic)1611-3349
ISBN (Print)978-3-030-29006-1
Publication statusPublished - Sep 2019
EventThe 12th International Symposium on Frontiers of Combining Systems - London, United Kingdom
Event duration: 4 Sep 20196 Sep 2019

Publication series

ISSN (Electronic)1611-3349


ConferenceThe 12th International Symposium on Frontiers of Combining Systems
Abbreviated titleFroCoS 2019
CountryUnited Kingdom