Editing Boolean satisfiability problem (section)

==Special cases of SAT==

===Conjunctive normal form===
Conjunctive normal form (in particular with 3 literals per clause) is often considered the canonical representation for SAT formulas. As shown above, the general SAT problem reduces to 3-SAT, the problem of determining satisfiability for formulas in this form.

===Disjunctive normal form===
SAT is trivial if the formulas are restricted to those in '''[[disjunctive normal form]]''', that is, they are a disjunction of conjunctions of literals. Such a formula is indeed satisfiable if and only if at least one of its conjunctions is satisfiable, and a conjunction is satisfiable if and only if it does not contain both ''x'' and NOT ''x'' for some variable ''x''. This can be checked in linear time. Furthermore, if they are restricted to being in '''full disjunctive normal form''', in which every variable appears exactly once in every conjunction, they can be checked in constant time (each conjunction represents one satisfying assignment).  But it can take exponential time and space to convert a general SAT problem to disjunctive normal form; to obtain an example, exchange "∧" and "∨" in the [[#Definitions|above]] exponential blow-up example for conjunctive normal forms.

===Exactly-1 3-satisfiability===
{{Main|1-in-3-SAT}}

Another NP-complete variant of the 3-satisfiability problem is the '''one-in-three 3-SAT''' (also known variously as '''1-in-3-SAT''' and '''exactly-1 3-SAT'''). Given a conjunctive normal form with three literals per clause, the problem is to determine whether there exists a truth assignment to the variables so that each clause has ''exactly'' one TRUE literal (and thus exactly two FALSE literals).

===Not-all-equal 3-satisfiability===
{{main|Not-all-equal 3-satisfiability}}
Another variant is the '''not-all-equal 3-satisfiability''' problem (also called '''NAE3SAT'''). Given a conjunctive normal form with three literals per clause, the problem is to determine if an assignment to the variables exists such that in no clause all three literals have the same truth value. This problem is NP-complete, too, even if no negation symbols are admitted, by Schaefer's dichotomy theorem.<ref name="schaefer">{{Cite conference | last1 = Schaefer | first1 = Thomas J. | year = 1978 | title = The complexity of satisfiability problems | book-title = Proceedings of the 10th Annual ACM Symposium on Theory of Computing | place = San Diego, California | pages = 216–226 | url = http://www.ccs.neu.edu/home/lieber/courses/csg260/f06/materials/papers/max-sat/p216-schaefer.pdf |doi=10.1145/800133.804350 |citeseerx=10.1.1.393.8951 }}</ref>

=== Linear SAT ===
A 3-SAT formula is ''Linear SAT'' (''LSAT'') if each clause (viewed as a set of literals) intersects at most one other clause, and, moreover, if two clauses intersect, then they have exactly one literal in common. An LSAT formula can be depicted as a set of disjoint semi-closed intervals on a line. Deciding whether an LSAT formula is satisfiable is NP-complete.<ref>{{Cite journal|last1=Arkin|first1=Esther M.|last2=Banik|first2=Aritra|last3=Carmi|first3=Paz|last4=Citovsky|first4=Gui|last5=Katz|first5=Matthew J.|last6=Mitchell|first6=Joseph S. B.|last7=Simakov|first7=Marina|date=2018-12-11|title=Selecting and covering colored points|journal=Discrete Applied Mathematics|language=en|volume=250|pages=75–86|doi=10.1016/j.dam.2018.05.011|issn=0166-218X|doi-access=free}}</ref>

===2-satisfiability===
{{Main|2-satisfiability}}

SAT is easier if the number of literals in a clause is limited to at most 2, in which case the problem is called '''[[2-SAT]]'''. This problem can be solved in polynomial time, and in fact is [[NL-complete|complete]] for the complexity class [[NL (complexity)|NL]]. If additionally all OR operations in literals are changed to [[Exclusive or|XOR]] operations, then the result is called '''exclusive-or 2-satisfiability''', which is a problem complete for the complexity class [[SL (complexity)|SL]] = [[L (complexity)|L]].

===Horn-satisfiability===
{{Main|Horn-satisfiability}}

The problem of deciding the satisfiability of a given conjunction of [[Horn clause]]s is called '''Horn-satisfiability''', or '''HORN-SAT'''. It can be solved in polynomial time by a single step of the [[unit propagation]] algorithm, which produces the single minimal model of the set of Horn clauses (w.r.t. the set of literals assigned to TRUE). Horn-satisfiability is [[P-complete]]. It can be seen as [[P (complexity)|P's]] version of the Boolean satisfiability problem. Also, deciding the truth of quantified Horn formulas can be done in polynomial time.<ref name="buningkarpinski">{{Cite journal | last1 = Buning | first1 = H.K. | last2 = Karpinski| first2 =  Marek| last3=Flogel|first3=A.|year = 1995 | title = Resolution for Quantified Boolean Formulas | journal = Information and Computation | volume = 117 | issue = 1 | pages = 12–18 | publisher = Elsevier | doi= 10.1006/inco.1995.1025| doi-access = free }}</ref>

Horn clauses are of interest because they are able to express [[Entailment|implication]] of one variable from a set of other variables. Indeed, one such clause ¬''x''<sub>1</sub> ∨ ... ∨ ¬''x''<sub>''n''</sub> ∨ ''y'' can be rewritten as ''x''<sub>1</sub> ∧ ... ∧ ''x''<sub>''n''</sub> → ''y''; that is, if ''x''<sub>1</sub>,...,''x''<sub>''n''</sub> are all TRUE, then ''y'' must be TRUE as well.

A generalization of the class of Horn formulas is that of renameable-Horn formulae, which is the set of formulas that can be placed in Horn form by replacing some variables with their respective negation. For example, (''x''<sub>1</sub> ∨ ¬''x''<sub>2</sub>) ∧ (¬''x''<sub>1</sub> ∨ ''x''<sub>2</sub> ∨ ''x''<sub>3</sub>) ∧ ¬''x''<sub>1</sub> is not a Horn formula, but can be renamed to the Horn formula (''x''<sub>1</sub> ∨ ¬''x''<sub>2</sub>) ∧ (¬''x''<sub>1</sub> ∨ ''x''<sub>2</sub> ∨ ¬''y''<sub>3</sub>) ∧ ¬''x''<sub>1</sub> by introducing ''y''<sub>3</sub> as negation of ''x''<sub>3</sub>. In contrast, no renaming of (''x''<sub>1</sub> ∨ ¬''x''<sub>2</sub> ∨ ¬''x''<sub>3</sub>) ∧ (¬''x''<sub>1</sub> ∨ ''x''<sub>2</sub> ∨ ''x''<sub>3</sub>) ∧ ¬''x''<sub>1</sub> leads to a Horn formula. Checking the existence of such a replacement can be done in linear time; therefore, the satisfiability of such formulae is in P as it can be solved by first performing this replacement and then checking the satisfiability of the resulting Horn formula.

{| style="float:right"
| [[File:Boolean satisfiability vs true literal counts.png|thumb|x200px|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.]]
|}

===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'')}}

===Schaefer's dichotomy theorem===
{{Main|Schaefer's dichotomy theorem}}
The restrictions above (CNF, 2CNF, 3CNF, Horn, XOR-SAT) bound the considered formulae to be conjunctions of subformulas; each restriction states a specific form for all subformulas: for example, only binary clauses can be subformulas in 2CNF.

Schaefer's dichotomy theorem states that, for any restriction to Boolean functions that can be used to form these subformulas, the corresponding satisfiability problem is in P or NP-complete.  The membership in P of the satisfiability of 2CNF, Horn, and XOR-SAT formulae are special cases of this theorem.<ref name="schaefer"/>

The following table summarizes some common variants of SAT.
{| class="wikitable sortable"
|+
!Code
!Name
!Restrictions
!Requirements
!Class
|-
|3SAT
|3-satisfiability
|Each clause contains 3 literals.
|At least one literal must be true.
|NP-c
|-
|2SAT
|2-satisfiability
|Each clause contains 2 literals.
|At least one literal must be true.
|NL-c
|-
|1-in-3-SAT
|Exactly-1 3-SAT
|Each clause contains 3 literals.
|Exactly one literal must be true.
|NP-c
|-
|1-in-3-SAT+
|Exactly-1 Positive 3-SAT
|Each clause contains 3 positive literals.
|Exactly one literal must be true.
|NP-c
|-
|NAE3SAT
|Not-all-equal 3-satisfiability
|Each clause contains 3 literals.
|Either one or two literals must be true.
|NP-c
|-
|NAE3SAT+
|Not-all-equal positive 3-SAT
|Each clause contains 3 positive literals.
|Either one or two literals must be true.
|NP-c
|-
|PL-SAT
|[[Planar SAT]]
|The incidence graph (clause-variable graph) is [[Planar graph|planar]].
|At least one literal must be true.
|NP-c
|-
|LSAT
|Linear SAT
|Each clause contains 3 literals, intersects at most one other clause, and the intersection is exactly one literal.
|At least one literal must be true.
|NP-c
|-
|HORN-SAT
|Horn satisfiability
|Horn clauses (at most one positive literal).
|At least one literal must be true.
|P-c
|-
|XOR-SAT
|Xor satisfiability
|Each clause contains XOR operations rather than OR.
|The XOR of all literals must be true.
|P
|}