XOR-SAT

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.^[a] XOR-SAT is in P,^[1] 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;^[2]. 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^[b]:

(a ⊕ b) ∧ (a) ∧ (b)

Here is a satisfiable XOR-SAT instance of 2 variables and 1 clause admitting 2 solutions:

(a ⊕ b)

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:

(a ⊕ b) ∧ (a)

Comparison with SAT variations

A formula with 2 clauses may be unsatisfied (red), 3-satisfied (green), xor-3-satisfied (blue), or/and 1-in-3-satisfied (yellow), depending on the TRUE-literal count in the 1st (hor) and 2nd (vert) clause.

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 red clause is optional):

(x₁ ⊕ ¬x₂ ⊕ x₄) ∧ (x₂ ⊕ x₄ ⊕ ¬x₃) ∧ (x₁ ⊕ x₂ ⊕ ¬x₃) ∧ (x₁ ⊕ x₂ ⊕ x₄)

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
	x1	⊕		x2	⊕		x4	≃ 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
	x1	⊕		x2	⊕		x4	≃ 1

If the red equation is present, it 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 red clause is present, the instance is unsolvable. Otherwise:

• x₁ = 1 = TRUE
• x₂ = 0 = FALSE
• x₃ = 1 = TRUE
• x₄ = 1 = TRUE

As a consequence, R(x₁, ¬x₂, x₄) ∧ R(x₂, x₄, ¬x₃) ∧ R(x₁, x₂, ¬x₃) ∧ R(¬x₁,x₂,x₄) is not 1-in-3-satisfiable, while (x₁ ∨ ¬x₂ ∨ x₄) ∧ (x₂ ∨ x₄ ∨ ¬x₃) ∧ (x₁ ∨ x₂ ∨ ¬x₃) ∧ (x₁ ∨ x₂ ∨ x₄) is 3-satisfiable with x₁=x₂=x₃=x₄=TRUE.

Notes

1. Formally, generalized conjunctive normal forms with a ternary Boolean function R are employed, which is TRUE just if 1 or 3 of its arguments is. An input clause with more than 3 literals can be transformed into an equisatisfiable conjunction of clauses á 3 literals similar to above; i.e. XOR-SAT can be reduced to XOR-3-SAT.
2. All the examples can be proved by the table of truth.