一种针对有限域与数组约束的组合方法
计算机科学中的逻辑
2013-12-03 v1 人工智能
软件工程
摘要
数组在软件验证中无处不在。然而，在约束规划 (CP) 中，针对数组的有效推理仍然罕见，因为局部推理对于数组约束而言条件极差。本文提出了一种结合全局符号推理与局部一致性过滤的方法，以求解涉及数组（包含访问、更新和尺寸约束）及其元素和索引上的有限域约束的约束系统。我们的方法名为 FDCC，基于标准数组理论的同余闭包算法与有限域 CP 求解器的组合。工作的难点在于两个求解器之间的双向通信机制。我们确定了需要共享的重要信息，并设计了控制通信开销的方法。在随机实例上的实验表明，FDCC 比两种求解器孤立使用的任何组合组合都能求解更多的公式，同时保持了合理的开销。
引用
@article{arxiv.1312.0200,
title = {A Combined Approach for Constraints over Finite Domains and Arrays},
author = {Sébastien Bardin and Arnaud Gotlieb},
journal= {arXiv preprint arXiv:1312.0200},
year = {2013}
}