Satisfiability of Non-linear (Ir)rational Arithmetic

9 years 5 months ago
Satisfiability of Non-linear (Ir)rational Arithmetic
Abstract. We present a novel way for reasoning about (possibly ir)rational quantifier-free non-linear arithmetic by a reduction to SAT/SMT. The approach is incomplete and dedicated to satisfiable instances only but is able to produce models for satisfiable problems quickly. These characteristics suffice for applications such as termination analysis of rewrite systems. Our prototype implementation, called MiniSmt, is made freely available. Extensive experiments show that it outperforms current SMT solvers especially on rational and irrational domains. Key words: non-linear arithmetic, SMT solving, term rewriting, termination, matrix interpretations.
Harald Zankl, Aart Middeldorp
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where LPAR
Authors Harald Zankl, Aart Middeldorp
Comments (0)