boolean-logic - （正）标准形式的 XOR 子句

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。因此它们在逻辑上是等价的。