(正)标准形式的异或子句

Question

我正在努力进行以下 XOR 子句转换：

给出以下 XOR 子句：

(x1 ⊕ ¬x2 ⊕ x3)

翻译成CNF，它是：

(¬x1 ∨ ¬x2 ∨ ¬x3)∧(¬x1 ∨ x2 ∨ x3)∧(x1 ∨ ¬x2 ∨ x3)∧(x1 ∨ x2 ∨ ¬x3)

这一点很清楚。

但是为什么(x1 ⊕ ¬x2 ⊕ x3) = (x1 ⊕ x2 ⊕ x3 ⊕ 1)？<-这被称为"标准形式"的XOR子句

为什么(x1 ⊕ x2 ⊕ x3 ⊕ 1) <=> x1 ⊕ x2 ⊕ x3 = 0？

我不明白...

这是我得到的论文中的另一句话："如果一个异或子句的所有文字都出现在正相中，那么它就是标准形式。

Answer 1

你需要证明(x1 ⊕ ¬x2 ⊕ x3) = (x1 ⊕ x2 ⊕ x3 ⊕ 1)

以 RHS 为例，

(x1 ⊕ x2 ⊕ x3 ⊕ 1) 
(x1 ⊕ x2 ⊕ 1 ⊕ x3) (⊕ is associative)
(x1 ⊕ ((x2 ∧ ¬1) ∨ (¬x2 ∧ 1)) ⊕ x3) (⊕ definition)
(x1 ⊕ (0 ∨ (¬x2 ∧ 1)) ⊕ x3) (Null)
(x1 ⊕ (¬x2 ∧ 1) ⊕ x3) (Identity)
(x1 ⊕ ¬x2 ⊕ x3) (Identity)

这等于LHS。因此，它们在逻辑上是等价的。