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.

BibTeX

@inproceedings{HZAM-LPAR09,
  author      = "Harald Zankl and Aart Middeldorp",
  title       = "Satisfiability of Non-Linear (Ir)rational Arithmetic",
  booktitle   = "Proceedings of the 16th International Conference on
                 Logic for Programming and Automated Reasoning",
  volume      = 6355,
  pages       = "481--500",
  year        = 2010
}