基于参数化解界限的量词-free Presburger公式判定

给定量词-free Presburger算式,若其有满足解,则必存在一个其大小(按位数衡量)在公式大小的多项式界限内的满足解。本文考虑一类特殊的量词-free Presburger算式,其中大多数线性约束为差(间隔)约束,而非差约束稀疏。该类在软件验证中常见。我们推导了以描述线性约束稀疏性和非差约束数量的额外参数为界限的新解界限。特别地,我们指出,每个整数变量所需的位数仅与非差约束数量成正比,与非差约束中非零系数的数量和大小的对数成正比,但与公式中总线性约束数无关。所得界限可用于基于在有限域上实例化整数变量并将输入量词-free Presburger算式转化为等满意性布尔算式的判定程序。除我们的主要理论结果外,我们讨论了若干优化措施,以在实际中获得更紧的界限。实证结果表明,我们的判定程序在其他判定程序之上可显著提升性能。