cl-banner

Satisfiability of Non-Linear (Ir)rational Arithmetic

Harald Zankl and Aart Middeldorp

Proceedings of the 16th International Conference on Logic for Programming and Automated Reasoning (LPAR-16), Lecture Notes in Artificial Intelligence 6355, pp. 481 – 500, 2010.

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 implementa-tion, called MiniSmt, is made freely available. Extensive experiments show that it outperforms current SMT solvers especially on rational and irrational domains.

 

  PDF |    doi:10.1007/978-3-642-17511-4_27  |  © Springer

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
}
Nach oben scrollen