首页> 外文期刊>Algorithmica >A Combinatorial Certifying Algorithm for Linear Feasibility in UTVPI Constraints
【24h】

A Combinatorial Certifying Algorithm for Linear Feasibility in UTVPI Constraints

机译:UTVPI约束中线性可行性的组合证明算法

获取原文
获取原文并翻译 | 示例

摘要

In this paper, we discuss a new combinatorial certifying algorithm for the problem of checking linear feasibility in Unit Two Variable Per Inequality (UTVPI) constraints. A UTVPI constraint has at most two non-zero variables and the coefficients of the non-zero variables belong to the set {+ 1, -1}. These constraints occur in a number of application domains, including but not limited to program verification, abstract interpretation, and operations research. The proposed algorithm runs in O(m center dot n) time and O(m + n) space on a UTVPI system with n variables and m constraints. Observe that these resource bounds match the bounds of the fastest strongly polynomial algorithm for difference constraints. Inasmuch as UTVPI constraints subsume difference constraints, it is clear that the resource requirements of our algorithm are optimal. Additionally, our algorithm is certifying, in that it produces a satisfying assignment when presented with a feasible instance, and a refutation, otherwise. At the heart of our algorithm is a new constraint network representation for UTVPI constraints.
机译:在本文中,我们讨论了一种新的组合证明算法,用于检查两个不等式变量(UTVPI)约束中的线性可行性问题。 UTVPI约束最多具有两个非零变量,并且非零变量的系数属于集合{+1,-1}。这些约束出现在许多应用程序领域中,包括但不限于程序验证,抽象解释和运筹学。该算法在具有n个变量和m个约束的UTVPI系统上的O(m中心点n)时间和O(m + n)空间中运行。请注意,这些资源范围与差异约束最快的强多项式算法的范围匹配。由于UTVPI约束包含差异约束,因此很明显,我们算法的资源需求是最优的。此外,我们的算法具有证明意义,因为当出现可行实例时,它会产生令人满意的分配,否则就会产生反驳。我们算法的核心是针对UTVPI约束的新约束网络表示。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号