XOR-SAT

  1. Home
  2. Wiki

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

[edit]

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

[edit]
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

[edit]

Given formula (the red clause is optional):

(x1 ⊕ ¬x2 ⊕ x4) ∧ (x2 ⊕ x4 ⊕ ¬x3) ∧ (x1 ⊕ x2 ⊕ ¬x3) ∧ (x1 ⊕ x2 ⊕ x4)

Equation system

[edit]

"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

[edit]

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

[edit]
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

[edit]
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

[edit]
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

[edit]

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

[edit]

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.

Notes

[edit]
  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.

References

[edit]
  1. ^ Schaefer, Thomas J. (1978). "The complexity of satisfiability problems". Proceedings of the tenth annual ACM symposium on Theory of computing - STOC '78. pp. 216–226. doi:10.1145/800133.804350.
  2. ^ Moore, Cristopher; Mertens, Stephan (2011), The Nature of Computation, Oxford University Press, p. 366, ISBN 9780199233212.