Abstract | ||
---|---|---|
ksmt is a CDCL-style calculus for solving non-linear constraints over the 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. |
Year | DOI | Venue |
---|---|---|
2021 | 10.1007/978-3-030-79876-5_7 | AUTOMATED DEDUCTION, CADE 28 |
DocType | Volume | ISSN |
Conference | 12699 | 0302-9743 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Franz Brauße | 1 | 0 | 1.01 |
Konstantin Korovin | 2 | 288 | 20.64 |
Margarita V. Korovina | 3 | 84 | 15.61 |
Norbert Th. Müller | 4 | 0 | 0.34 |