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

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):

(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.

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.

References

  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.
This article is issued from Wikipedia. The text is available under Creative Commons Attribution-Share Alike 4.0 unless otherwise noted. Additional terms may apply for the media files.