algorithm - 将图形可达性降低到 SAT (CNF)

Question

所以我在教科书上遇到了这个问题。我想知道如何将图形可达性问题简化为 SAT (CNF) 问题。 (即如果图 G 中存在从开始到结束节点的路径，则公式是可满足的)

1) 我不知道如何从可以在多项式时间内解决的问题(图可达性)转变为 NP (SAT)。

2) 我似乎无法找到一种方法来将 Graph 的这些节点/边表述为 CNF 中对应于可达性的实际子句。

我尝试考虑像 Floyd-Warshall 这样的算法来确定是否存在从开始到结束节点的路径，但我似乎无法将该想法表述为实际的 CNF 子句。非常感谢您的帮助!

Answer 1

想出您所期望的答案可能不会太难，但这里是真正的答案:

将问题X“减少”为问题Y意味着将X的任何实例转换为Y的实例> 这样，Y 的答案就是X 的答案。通常，我们要求 P-time reduction，即问题的转换和答案的提取都必须在多项式时间内发生。

Graph Reachability 很容易在线性时间内解决，这当然是多项式时间，因此从 Graph Reachability 到 SAT 的简化非常简单:

1. 给定一个图的可达性问题，在线性时间内求解；
2. 如果所需路径存在，写出任何可满足的 SAT 实例，如 (A)。否则，写出任何无法满足的 SAT 实例，如 (A)&(~A)