The boolean
xor operation
Derivation of the Tseitin transformation:
O ≡ A ⊕ B
O ≡ ((¬A & B) | (A & ¬B))
(O → ((¬A & B) | (A & ¬B))) & (¬O → ¬((¬A & B) | (A & ¬B)))
Left hand side:
O → ((¬A & B) | (A & ¬B))
¬O | ((¬A & B) | (A & ¬B))
¬O | ((¬A | A) & (¬A | ¬B) & (A | B) & (¬B | B))
¬O | ((¬A | ¬B) & (A | B))
(¬O | ¬A | ¬B) & (¬O | A | B)
Right hand side:
¬O → ¬((¬A & B) | (A & ¬B))
O | ¬((¬A & B) | (A & ¬B))
O | (¬(¬A & B) & ¬(A & ¬B))
O | ((A | ¬B) & (¬A | B))
(O | ¬A | B) & (O | A | ¬B)
Result:
(¬O | ¬A | ¬B) & (¬O | A | B) & (O | ¬A | B) & (O | A | ¬B)