CODEWITHSUNDEEP
boolean-logicxorsolversatsatisfiability
random-user
random-user

Reputation: 47

XOR clause in (positive) standard form

I'm struggling with following XOR clause transformation:

This XOR clause is given:

(x1 ⊕ ¬x2 ⊕ x3)

translated into CNF, it is:

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

This is clear.

But why is (x1 ⊕ ¬x2 ⊕ x3) = (x1 ⊕ x2 ⊕ x3 ⊕ 1) ? <-this is called the XOR clause in "standard form"

and why is (x1 ⊕ x2 ⊕ x3 ⊕ 1) <=> x1 ⊕ x2 ⊕ x3 = 0?

I don't get it...

Here's another quote from the paper I got this: "An xor-clause is in the standard form if all of its literals appear in the positive phase."

Upvotes: 2

Views: 784

Answers (1)

Zachary
Zachary

Reputation: 1703

You need to prove (x1 ⊕ ¬x2 ⊕ x3) = (x1 ⊕ x2 ⊕ x3 ⊕ 1)

Take the 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)

Which is equal to the LHS. Hence they are logically equivalent.

Upvotes: 2

Related Questions