（正）标准形式的 XOR 子句
XOR clause in (positive) standard form
我正在努力进行以下 XOR 子句转换：
给出这个异或子句：
(x1 ⊕ ¬x2 ⊕ x3)
翻译成CNF就是：
(¬x1 ∨ ¬x2 ∨ ¬x3)∧(¬x1 ∨ x2 ∨ x3)∧(x1 ∨ ¬x2 ∨ x3)∧(x1 ∨ x2 ∨ ¬x3)
这就清楚了。
但为什么是 (x1 ⊕ ¬x2 ⊕ x3) = (x1 ⊕ x2 ⊕ x3 ⊕ 1)？ <-这在 "standard form"
中称为 XOR 子句
为什么是 (x1 ⊕ x2 ⊕ x3 ⊕ 1) <=> x1 ⊕ x2 ⊕ x3 = 0？
我不明白...
这是我从论文中得到的另一句话："An xor-clause is in the standard form if all of its literals appear in the positive phase."
你需要证明(x1 ⊕ ¬x2 ⊕ x3) = (x1 ⊕ x2 ⊕ x3 ⊕ 1)
走右手边，
(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)
等于左轴。因此它们在逻辑上是等价的。
我正在努力进行以下 XOR 子句转换：
给出这个异或子句：
(x1 ⊕ ¬x2 ⊕ x3)
翻译成CNF就是：
(¬x1 ∨ ¬x2 ∨ ¬x3)∧(¬x1 ∨ x2 ∨ x3)∧(x1 ∨ ¬x2 ∨ x3)∧(x1 ∨ x2 ∨ ¬x3)
这就清楚了。
但为什么是 (x1 ⊕ ¬x2 ⊕ x3) = (x1 ⊕ x2 ⊕ x3 ⊕ 1)？ <-这在 "standard form"
为什么是 (x1 ⊕ x2 ⊕ x3 ⊕ 1) <=> x1 ⊕ x2 ⊕ x3 = 0？
我不明白...
这是我从论文中得到的另一句话："An xor-clause is in the standard form if all of its literals appear in the positive phase."
你需要证明(x1 ⊕ ¬x2 ⊕ x3) = (x1 ⊕ x2 ⊕ x3 ⊕ 1)
走右手边，
(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)
等于左轴。因此它们在逻辑上是等价的。