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. 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).
01Examples
Here is an unsatisfiable XOR-SAT instance of 2 variables and 3 clauses:
- (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)
02Comparison 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.
03Solving an XOR-SAT example by Gaussian elimination
Given formula (the red clause is optional):
(x1 ⊕ ¬x2 ⊕ x4) ∧ (x2 ⊕ x4 ⊕ ¬x3) ∧ (x1 ⊕ x2 ⊕ ¬x3) ∧ (x1 ⊕ x2 ⊕ x4)
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:
- 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) ∧ R(¬x1,x2,x4) 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.
Sources and credits
This article is adapted from the Wikipedia article “XOR-SAT”, written by its contributors and licensed under CC BY-SA 4.0. Fathomly has changed the layout, removed citation markers, navigation and maintenance notices, and adjusted punctuation. This adapted version is shared under the same license. For references, see the original article.
Images, from Wikimedia Commons:
- Boolean satisfiability vs true literal counts.png by Jochen Burghardt, CC BY-SA 3.0
Fathomly is not affiliated with or endorsed by the Wikimedia Foundation. Spotted a problem? Tell us.