algorithm - 在 2-SAT 问题中将 CNF 转换为命令式范式的解释？

Question

所以这个问题对你们中的许多人来说可能看起来很愚蠢，但我发现很难掌握 CNF 子句到 INF 子句的转换。

我正在阅读这篇文章，其中指出：

首先，我们需要将问题转换为不同的形式，即所谓的隐式范式。请注意，表达式 a∨b 等价于¬a⇒b∧¬b⇒a（如果两个变量之一为假，则另一个必须为真）。

有人可以解释我们如何得到这个结果/这种转换如何有意义？我也不知道“=>”符号是什么意思。提前致谢！

更新 1：如果对不同的逻辑符号有疑问，请参阅此wiki。

Answer 1

=>是蕴涵，带有真值表：

A B | A => B
----+-------
F F |   T
F T |   T
T F |   F
T T |   T

事实上，你可以证明a => b等价于~a \/ b。（只需填写真值表。）

现在，我们有：

  ~a => b 
= ~(~a) \/ b
= a \/ b

所以，它甚至更强大：a \/ b相当于~a => b. 您可以类似地证明它也等价于~b => a; 所以取连词可能是多余的，但它不会改变等价性。

如果有疑问，请始终绘制完整的真值表，假设您有 4-5 个变量，这将非常有教育意义。如果您有更多变量，请使用 SAT/SMT 求解器来证明等价性。这就是他们的好处。