> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/300-logic/terms/sat-problem.md).

# Boolean satisfiability problem

<https://en.wikipedia.org/wiki/Satisfiability> <https://en.wikipedia.org/wiki/Boolean_satisfiability_problem>

In CS, the Boolean satisfiability problem (sometimes called *propositional satisfiability problem* and abbreviated as *SATISFIABILITY* or *SAT*) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula.

In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE.

If this is the case, the formula is called *satisfiable*. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is *unsatisfiable*.

For example, the formula `a AND NOT b` is satisfiable because one can find the values `a = TRUE` and `b = FALSE`, which make `(a AND NOT b) = TRUE`. In contrast, `a AND NOT a` is unsatisfiable.

## Basic definitions and terminology

A propositional logic formula (Boolean expression) is built from:

* variables
* operator AND (conjunction, ∧)
* operator  OR (disjunction, ∨)
* operator NOT (negation, ¬)
* parentheses

A formula is said to be satisfiable if it can be made TRUE by assigning appropriate logical values (i.e. TRUE, FALSE) to its variables.

> The Boolean satisfiability problem (SAT) is, given a formula, to check whether it is satisfiable.

There are several special cases of the Boolean satisfiability problem in which the formulas are required to have a particular structure.

Literals:

* *positive literal*: variable
* *negative literal*: negation of a variable
* **Clause** is a *disjunction* of literal(s).
* **Horn clause** if a clause contains at most one positive literal.
* **Conjunctive Normal Form (CNF)**: formula that is a *conjunction* of clause(s).

**Conjunctive normal form** (CNF): in Boolean logic, a formula is in Conjunctive Normal Form (or Clausal Normal Form) if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is an **AND of ORs**.

For example: `x1` is a positive literal, `¬x2` is a negative literal, `x1 ∨ ¬x2` is a clause, and `(x1 ∨ ¬x2) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1` is a formula in CNF.

The first and third clauses are Horn clauses, but its second clause is not. The formula is satisfiable by choosing `x1 = F`, `x2 = F`, and `x3` arbitrarily, since: `(F ∨ ¬F) ∧ (¬F ∨ F ∨ x3) ∧ ¬F` evaluates to `(F ∨ T) ∧ (T ∨ F ∨ x3) ∧ T`, and in turn to `T ∧ T ∧ T` (i.e. to `TRUE`).

In contrast, the CNF formula `a ∧ ¬a`, consisting of two clauses of one literal, is unsatisfiable, since for `a=T` or `a=F` it evaluates to `T ∧ ¬T` (i.e., `F`) or `F ∧ ¬F` (i.e. again `F`), respectively.