Editing Boolean satisfiability problem (section)

===XOR-satisfiability===

{| align="right" class="wikitable collapsible collapsed" style="text-align:left; margin: 1em; max-width: 95%"
|-
! Solving an XOR-SAT example<BR>by [[Gaussian elimination]]
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! Given formula
|-
| ("⊕" means XOR, the {{color|#ff8080|red clause}} is optional)
|-
| (''a''⊕''c''⊕''d'') ∧ (''b''⊕¬''c''⊕''d'') ∧ (''a''⊕''b''⊕¬''d'') ∧ (''a''⊕¬''b''⊕¬''c'') {{color|#ff8080|∧ (¬''a''⊕''b''⊕''c'')}}
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="9" | Equation system
|-
| colspan="9" | ("1" means TRUE, "0" means FALSE)
|-
| colspan="9" | Each clause leads to one equation.
|-
|  || ''a'' || ⊕ ||   || ''c'' || ⊕ ||   || ''d'' || = 1
|-
|  || ''b'' || ⊕ || ¬ || ''c'' || ⊕ ||   || ''d'' || = 1
|-
|  || ''a'' || ⊕ ||   || ''b'' || ⊕ || ¬ || ''d'' || = 1
|-
|  || ''a'' || ⊕ || ¬ || ''b'' || ⊕ || ¬ || ''c'' || = 1
|-
|  {{color|#ff8080|¬}} || {{color|#ff8080|''a''}} || {{color|#ff8080|⊕}} || || {{color|#ff8080|''b''}} || {{color|#ff8080|⊕}} || || {{color|#ff8080|''c''}} || {{color|#ff8080| ≃ 1}}
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="6" | Normalized equation system
|-
| colspan="6" | using properties of [[Boolean rings]] (¬''x''=1⊕''x'', ''x''⊕''x''=0)
|-
| ''a'' || ⊕ || ''c'' || ⊕ || ''d'' || = '''1'''
|-
| ''b'' || ⊕ || ''c'' || ⊕ || ''d'' || = '''0'''
|-
| ''a'' || ⊕ || ''b'' || ⊕ || ''d'' || = '''0'''
|-
| ''a'' || ⊕ || ''b'' || ⊕ || ''c'' || = '''1'''
|-
| {{color|#ff8080|''a''}} || {{color|#ff8080|⊕}}  || {{color|#ff8080|''b''}} || {{color|#ff8080|⊕}} || {{color|#ff8080|''c''}} || {{color|#ff8080| ≃ '''0'''}}
|-
| colspan="6" | (If the {{color|#ff8080|red equation}} is present, {{color|#ff8080|it}} contradicts
|-
| colspan="6" | the last black one, so the system is unsolvable.
|-
| colspan="6" | Therefore, Gauss' algorithm is
|-
| colspan="6" | used only for the black equations.)
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="6" | Associated coefficient matrix
|-
| &nbsp;
|-
! ''a'' !! ''b'' !! ''c'' !! ''d'' !!   !! line
|-
| &nbsp;
|-
| 1 || 0 || 1 || 1
! 1
| A
|-
| 0 || 1 || 1 || 1
! 0
| B
|-
| 1 || 1 || 0 || 1
! 0
| C
|-
| 1 || 1 || 1 || 0
! 1
| D
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="6" |Transforming to echelon form
|-
| &nbsp;
|-
! ''a'' !! ''b'' !! ''c'' !! ''d'' !!   !! operation
|-
| &nbsp;
|-
| 1 || 0 || 1 || 1
! 1
| A
|-
| 1 || 1 || 0 || 1
! 0
| C
|-
| 1 || 1 || 1 || 0
! 1
| D
|-
| 0 || 1 || 1 || 1
! 0
| B (swapped)
|-
| &nbsp;
|-
| 1 || 0 || 1 || 1
! 1
| A
|-
| 0 || 1 || 1 || 0
! 1
| E = C⊕A
|-
| 0 || 1 || 0 || 1
! 0
| F = D⊕A
|-
| 0 || 1 || 1 || 1
! 0
| B
|-
| &nbsp;
|-
| 1 || 0 || 1 || 1
! 1
| A
|-
| 0 || 1 || 1 || 0
! 1
| E
|-
| 0 || 0 || 1 || 1
! 1
| G = F⊕E
|-
| 0 || 0 || 0 || 1
! 1
| H = B⊕E
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="6" | Transforming to diagonal form
|-
| &nbsp;
|-
! ''a'' !! ''b'' !! ''c'' !! ''d'' !!   !! operation
|-
| &nbsp;
|-
| 1 || 0 || 1 || 0
! 0
| I = A⊕H
|-
| 0 || 1 || 1 || 0
! 1
| E
|-
| 0 || 0 || 1 || 0
! 0
| J = G⊕H
|-
| 0 || 0 || 0 || 1
! 1
| H
|-
| &nbsp;
|-
| 1 || 0 || 0 || 0
! 0
| K = I⊕J
|-
| 0 || 1 || 0 || 0
! 1
| L = E⊕J
|-
| 0 || 0 || 1 || 0
! 0
| J
|-
| 0 || 0 || 0 || 1
! 1
| H
|-
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! Solution:
|-
| If the {{color|#ff8080|red clause}} is present: || Unsolvable
|-
| Else: || ''a'' = 0 = FALSE
|-
| || ''b'' = 1 = TRUE
|-
| || ''c'' = 0 = FALSE
|-
| || ''d'' = 1 = TRUE
|-
| colspan="2" | '''As a consequence:'''
|-
| colspan="2" | ''R''(''a'',''c'',''d'') ∧ ''R''(''b'',¬''c'',''d'') ∧ ''R''(''a'',''b'',¬''d'') ∧ ''R''(''a'',¬''b'',¬''c'') {{color|#ff8080|∧ ''R''(¬''a'',''b'',''c'')}}
|-
| colspan="2" | is not 1-in-3-satisfiable,
|-
| colspan="2" | while (''a'' ∨ ''c'' ∨ ''d'') ∧ (''b'' ∨ ¬''c'' ∨ ''d'') ∧ (''a'' ∨ ''b'' ∨ ¬''d'') ∧ (''a'' ∨ ¬''b'' ∨ ¬''c'')
|-
| colspan="2" |  is 3-satisfiable with ''a''=''c''=FALSE and ''b''=''d''=TRUE.
|}
|}

Another special case is the class of problems where each clause contains XOR (i.e. [[exclusive or]]) rather than (plain) OR operators.{{efn|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 [[#3-satisfiability|above]]; i.e. XOR-SAT can be reduced to XOR-3-SAT.}} This is in [[P (complexity class)|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]];<ref>{{citation|title=The Nature of Computation|first1=Cristopher|last1=Moore|author1-link=Cristopher Moore|first2=Stephan|last2=Mertens|publisher=Oxford University Press|year=2011|isbn=9780199233212|page=366|url=https://books.google.com/books?id=z4zMiZyAE1kC&pg=PA366}}.</ref> see the box for an example. This recast is based on the [[Boolean algebra (structure)#Boolean rings|kinship between Boolean algebras and Boolean rings]], and the fact that arithmetic modulo two forms the finite field [[GF(2)]]. Since ''a'' XOR ''b'' XOR ''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 [[P = NP problem|complexity classes P and NP are not equal]], neither 2-, nor Horn-, nor XOR-satisfiability is NP-complete, unlike SAT.

====Examples====
Here is an unsatisfiable XOR-SAT instance of 2 variables and 3 clauses:
:{{math|(''a'' ⊕ ''b'') ∧ (''a'') ∧ (''b'')}}

Here is a satisfiable XOR-SAT instance of 2 variables and 1 clause admitting 2 solutions:
:{{math|(''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:
:{{math|(''a'' ⊕ ''b'') ∧ (''a'')}}