AI 中文总结
本文针对非线性整数算术SMT问题，提出改进的增量线性化公理集，基于Z3实现独立求解器，在SMT-LIB的NIA基准上整体性能与顶尖求解器相当，在多项式约束基准上表现更优。
AI 中文摘要
增量线性化此前已被提出用于求解无量词非线性整数算术的SMT问题，尽管概念简单但已被证明有效。本文引入了修订后的公理集，该公理集提升了针对由高次单项式（如幂项和混合乘积）构成的多项式约束的收敛性，而这类问题是此前公理化方法难以处理的。我们基于用于线性整数算术的Z3实现了独立版本，并在来自SMT-LIB的NIA基准集上进行评估。结果表明，该方法整体上可与最先进的求解器竞争，且在以这类多项式约束为主的基准上显著优于后者。
英文摘要
Incremental Linearization has previously been proposed for solving SMT problems over quantifier-free nonlinear integer arithmetic and has proven effective despite its conceptual simplicity. In this paper, we introduce a revised axiom set that improves convergence on polynomial constraints built from higher-degree monomials, such as powers and mixed products, a class of problems on which prior axiomatizations struggled. We present a standalone implementation built on top of Z3 for linear integer arithmetic and evaluate it on the NIA benchmark set from SMT-LIB. Our results show that the approach is competitive with state-of-the-art solvers overall and substantially outperforms them on benchmarks dominated by such polynomial constraints.
CommentsEPIA 2026 preprint
