整数八边形约束的改进紧闭包算法
数据结构与算法
2007-06-01 v2 计算几何
计算机科学中的逻辑
摘要
整数八边形约束（亦称“每不等式两变量单位”或“UTVPI整数约束”）构成了一类有趣的约束，用于在约束编程以及软件与硬件系统的形式分析与验证领域中表示和求解整数问题，因为它们将具有多项式复杂度的算法与相对较好的表达能力相结合。操作此类约束所需的主要算法是可满足性检验以及约束集推理闭包的计算。后者被称为“紧”闭包，以区别于不利用变量整数性的（不完全）闭包算法。在本文中，我们提出并充分论证了一种 O(n^3) 算法，用于计算一组 UTVPI 整数约束的紧闭包。
引用
@article{arxiv.0705.4618,
title = {An Improved Tight Closure Algorithm for Integer Octagonal Constraints},
author = {Roberto Bagnara and Patricia M. Hill and Enea Zaffanella},
journal= {arXiv preprint arXiv:0705.4618},
year = {2007}
}
评论
15 pages, 2 figures