In computational complexity, XOR-SAT (also known as XORSAT) is the class of boolean satisfiability problems where each clause contains XOR (i.e. exclusive or, written "⊕") rather than (plain) OR operators. XOR-SAT is in P, since an XOR-SAT formula can also be viewed as a system of linear equations mod 2, and can be solved in cubic time by Gaussian elimination;.. This recast is based on the kinship between Boolean algebras and Boolean rings, and the fact that arithmetic modulo two forms the finite field GF(2).
Examples Here is an unsatisfiable XOR-SAT instance of 2 variables and 3 clauses:
Here is a satisfiable XOR-SAT instance of 2 variables and 1 clause admitting 2 solutions:
And here is a unique XOR-SAT instance, that is to say a satisfiable XOR-SAT instance of 2 variables and 2 clauses admitting exactly one solution:
Comparison with SAT variations
Since a ⊕ b ⊕ c evaluates to TRUE if and only if exactly 1 or 3 members of {a,b,c} are TRUE, each solution of the 1-in-3-SAT problem for a given CNF formula is also a solution of the XOR-3-SAT problem, and in turn each solution of XOR-3-SAT is a solution of 3-SAT; see the picture. As a consequence, for each CNF formula, it is possible to solve the XOR-3-SAT problem defined by the formula, and based on the result infer either that the 3-SAT problem is solvable or that the 1-in-3-SAT problem is unsolvable.
Provided that the complexity classes P and NP are not equal, neither 2-, nor Horn-, nor XOR-satisfiability is NP-complete, unlike SAT.
Solving an XOR-SAT example by Gaussian elimination Given formula (the is optional):
(x1 ⊕ ¬x2 ⊕ x4) ∧ (x2 ⊕ x4 ⊕ ¬x3) ∧ (x1 ⊕ x2 ⊕ ¬x3)
Equation system "1" means TRUE, "0" means FALSE. Each clause leads to one equation.
x1 ⊕ ¬ x2 ⊕ x4 = 1 x2 ⊕ x4 ⊕ ¬ x3 = 1 x1 ⊕ x2 ⊕ ¬ x3 = 1
Normalized equation system Using properties of Boolean rings (¬x=1⊕x, x⊕x=0) x1 ⊕ x2 ⊕ x4 = 0 x2 ⊕ x4 ⊕ x3 = 0 x1 ⊕ x2 ⊕ x3 = 0
If the is present, contradicts the first black one, so the system is unsolvable. Therefore, Gauss' algorithm is used only for the black equations.
Associated coefficient matrix
x1 x2 x3 x4 line 1 1 0 1 0 A 0 1 1 1 0 B 1 1 1 0 0 C
Transforming to echelon form x1 x2 x3 x4 operation 1 1 0 1 0 A 0 1 1 1 0 B 0 0 1 1 0 D = C ⊕ A
Transforming to diagonal form x1 x2 x3 x4 operation 1 0 0 1 0 F = A ⊕ B ⊕ D 0 1 0 0 0 E = B ⊕ D 0 0 1 1 0 D
Variable random assignments For all the variables at the right of the diagonal form (if any), we assign any random value.
x1 x2 x3 x4=TRUE Result of the assigned values x1 TRUE FALSE x1 = TRUE x2 FALSE x2 = FALSE x3 TRUE FALSE x3 = TRUE
Solution If the is present, the instance is unsolvable. Otherwise: x1 = 1 = TRUE x2 = 0 = FALSE x3 = 1 = TRUE x4 = 1 = TRUE
As a consequence, R(x1, ¬x2, x4) ∧ R(x2, x4, ¬x3) ∧ R(x1, x2, ¬x3) is not 1-in-3-satisfiable, while (x1 ∨ ¬x2 ∨ x4) ∧ (x2 ∨ x4 ∨ ¬x3) ∧ (x1 ∨ x2 ∨ ¬x3) ∧ (x1 ∨ x2 ∨ x4) is 3-satisfiable with x1=x2=x3=x4=TRUE.
Notes
References