Satisfiability of Non-linear (Ir)rational Arithmetic
Satisfiability of Non-linear (Ir)rational Arithmetic
复制标题
非线性（Ir）有理算术的可满足性
DOI：
10.1007/978-3-642-17511-4_27
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
A. Middeldorp
中科院分区：
文献类型：
--
作者：
Harald Zankl;A. Middeldorp
我们提出了一种新的推理方式（可能是IR）理性量词自由非线性算术减少SAT/SMT。该方法是不完整的，并致力于满足的情况下，但能够满足问题的快速产生模型。这些特性足以应用于重写系统的终止分析。我们的原型实现，称为MiniSmt，是免费提供的。大量的实验表明，它优于目前的SMT求解器，特别是在合理和不合理的领域。
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.