Skip to Main content Skip to Navigation
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.
Complete list of metadata

https://hal.inria.fr/hal-01946733
Contributor : Pascal Fontaine Connect in order to contact the contributor
Submitted on : Thursday, December 6, 2018 - 12:35:39 PM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM
Long-term archiving on: : Thursday, March 7, 2019 - 1:23:11 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01946733, version 1

Collections

Citation

Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Van Khanh To, Xuan Tung Vu. Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT. SC-square 2018 - Third International Workshop on Satisfiability Checking and Symbolic Computation, Jul 2018, Oxford, United Kingdom. ⟨hal-01946733⟩

Share

Metrics

Record views

127

Files downloads

283