Finding Short Tree-Like Unit Refutations in UTVPI Constraint Systems

doi:10.1007/978-3-032-04587-4_10

2026-01-01

PRE

Piotr Wojciechowski

K. Subramani *

DOI：10.1007/978-3-032-04587-4_10

原文链接

原文求助

摘要

En 中文

本文研究了单位否定性在每不等式两个变量（UTVPI）约束系统（UCSs）中的表现。每不等式两个变量（UTVPI）约束是一种形式为±x(i)±x(j)≤b(ij)的线性关系，其中b(ij)是整数集Z的元素。UCS是此类约束的合取。若要求UTVPI约束中的两个变量符号相反，则该约束称为差分约束，此类约束的合取称为差分约束系统（DCS）。当决策过程判定UCS不可行时，提供证明其不可行性的证书至关重要，此类证书称为否定证书。否定（在适当的否定系统下）构成了否定证书的一个重要子类。复杂性类P中的所有问题都有简洁的否定证书。我们关注否定的一个子类，称为单位否定（UR）。UR否定系统是不完备的，即不可满足的UCS可能没有单位否定。然而，从识别导致系统不一致的变量域的角度来看，它们是有用的。先前的工作研究了UCS的类似有向无环图（dag）的单位否定[18]。本文考察了UCS的树形单位否定。

Keyword:

Unit Refutability

UTVPI Constraint Systems

Unit Refutations

Tree-Like Refutations

Constraint Satisfaction