| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT
Abstract : We report on a prototypical tool for Satisfiability Modulo Theory solving
for quantifier-free formulas in Non-linear Real Arithmetic or, more precisely,
real closed fields, which uses a computer algebra system as the main component.
This is complemented with two heuristic techniques, also stemming from
computer algebra, viz. interval constraint propagation and subtropical satisfiability.
Our key idea is to make optimal use of existing knowledge and work in the
symbolic computation community, reusing available methods and implementations
to the most possible extent. Experimental results show that our approach is
surprisingly efficient in practice.
https://hal.inria.fr/hal-01946733
Contributor : Pascal Fontaine <>
Submitted on : Thursday, December 6, 2018 - 12:35:39 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Document(s) archivé(s) le : Thursday, March 7, 2019 - 1:23:11 PM
Contributor : Pascal Fontaine <>
Submitted on : Thursday, December 6, 2018 - 12:35:39 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Document(s) archivé(s) le : Thursday, March 7, 2019 - 1:23:11 PM
File
main.pdf
Files produced by the author(s)