3

我有一堆约束，每个约束由两个符号和一个比较运算符组成：<, <=, !=, ==, >=, 或>。因此，例如：

A <= B
C >= B
A != C
C == D
D > E

我希望能够做三件事：

  1. 首先，我想检查是否有任何不一致之处。因此，例如，如果我有A > B、B > C和A == C，则存在不一致，因为A必须既等于C又大于它。
  2. 我希望能够查询任何两个符号，并取回它们之间可行的相对顺序。因此，例如query(A, C)应该返回{<}（由单个元素组成的集合：小于），并且query(B, E)应该返回{<, =, >}.
  3. 我希望能够添加一个约束（这也可以添加（一个）附加符号，例如添加F == G到上面的示例中）。

查询比添加约束更常见。

如果您没有任何!=限制，我已经想出了一个可行的方法：

  1. 将每个约束转换为仅使用<或<=（因此：X == Y变成X <= Yand Y <= X，X > Y变成Y < X等）的约束。
  2. 使用约束作为边，使用符号构建有向图。
  3. 对于图中的所有环，如果该环至少包含一条<边，则存在矛盾。

至query(X, Y)：

  1. X找到和之间的任何路径Y。
    • 如果没有这样的路径，这部分的结果是{<, =, >}。
    • 如果路径至少包含一个<，则这部分的结果是{<}.
    • 否则，这部分的结果是{<, =}。
  2. Y找到和之间的任何路径X
    • 如果没有这样的路径，这部分的结果是{<, =, >}。
    • 如果路径至少包含一个<，则这部分的结果是{>}.
    • 否则，这部分的结果是{=, >}。
  3. 结果是上述两个结果的并集。

（显然，我可以缓存查询，至少在我添加另一个约束之前）

我可以将此扩展到包含!=，但随后它会随着使用的约束数量成倍地变慢!=。（保留一组图而不是一个。每次添加约束时!=，对于集合中的每个图，将其替换为两个副本，一个要添加的约束是<，一个是>。任何时候都会产生矛盾，丢弃它。如果图集为空，则存在矛盾。在查询中，检查所有图，将答案合并在一起。）

那么，有没有更有效的方法来解决这个问题呢？还是无论如何都会成为指数级的最坏情况？

我知道我可以为此使用 SAT 求解器，但委婉地说，这似乎有点矫枉过正，特别是因为我看不到它超过 100 个约束，其中 10 个更典型。

（对于那些对此感兴趣的人，我正在研究一种玩具编程语言，并对制作自定义中缀运算符的想法感兴趣，其中优先级由与现有运算符的关系而不是直接数值决定（这有问题当您想添加一个优先级高于A但低于的新运算符时B，但两者之间没有差距。!=该问题并不严格要求，但我开始对如何包含它感兴趣。）

4

1 回答 1

3

有一些可爱的数学大意是，除非你能证明 A <= B 和 B <= A 使用自反性和传递性，否则存在一个模型 A != B。变量上的强制相等类一一对应与 <= 相关变量图的强连通分量（其中 A = B 导致 A <= B 和 B <= A）。

总而言之，确定可行性的算法是提取所有 <= 约束（其中 A < B 导致 A <= B，A = B 导致 A <= B 和 B <= A，A != B 什么也不导致)，在有向图中找到强分量，然后验证，对于每个 A < B 和 A != B，A 和 B 位于不同的强分量中。要查询，依次添加每种可能性并检查可行性。

于 2014-03-26T17:19:44.153 回答