This slideshow introduces and explains the "Formula Satisfiability" (SAT) Problem.


We start with some definitions and background.

Boolean variables are variables that can have a value from {T, F}, where 'T' stands for TRUE and 'F' for FALSE.
We typically use subscripts on letters like $x$ and $y$ for our Boolean variables: $x_1, x_2, x_3$

We use Boolean operators AND (+) , OR (.), and NOT ($\overline{\ \ }$ over a variable), which follow these truth tables:

The NOT Operator

The AND Operator

The OR Operator

A Boolean formula is composed of boolean variables and operators. For example: $x_1 + x_2 . \overline{x_3}$

A literal is either a boolean variable ($x$) or its negation ($\overline{x}$)

For example: $a, \overline{b} , \overline{g}, c, \overline{c}$.

A clause is a disjunction (OR) of literals such as $l_1 + l_2 + l_3 +\cdots +l_n$ for literals $l_i$.

For example:     ($a + \overline{b}$) ,      $\overline{g}$ ,      ($c + \overline{f} + \overline{e} + h$).

A Conjunctive normal form (CNF) is a conjunction (AND) of clauses.

For example:     $\overline{x_1} . (x_1 + x_2).(x_3 + x_4 + \overline{x_5}) . (x_1 + x_3) . (\overline{x_3} + x_2 + \overline{x_5}) . (x_1 + x_2 + \overline{x_3}) . (x_3 + x_4 + \overline{x_2}) . (\overline{x_4} + \overline{x_1} + \overline{x_5}) . (x_1 + x_3 + x_5)$

We will use CNF exclusively from now on.

An assignment to the Boolean variables in a formula is known as a truth assignment.

A truth assignment of variables is said to be satisfying, if it causes the formula to evaluate to "TRUE".

A CNF is said to be satisfiable if it has a satisfying assignment.

For example: $(x_1 + x_2 . x_3)$ is "True" for $x_1$=T , $x_2$=T, $x_3$=T , hence satisfiable.

($x_1 . \overline{x_1}$) is always "False", hence not satisfiable.

Given any boolean formula in CNF, is the formula satisfiable?

P = ($x_1$ + $x_2$).($x_2$ + $\overline{x_3}$ + $x_4$).($x_1$ + $\overline{x_2}$ + $x_3$ + $x_4$).($\overline{x_1}$ + $x_3$)

Truth Table for P

There exist assignments that makes the formula true (the green rows).

P is satisfiable.

P = ($x_1$ + $x_2$).($x_2$ + $\overline{x_3}$ + $x_4$).($x_3$ + $\overline{x_4}$).($x_1$ + $\overline{x_1}$).($x_1$ + $\overline{x_2}$ + $x_3$ + $x_4$)

Truth Table for P

There does not exist any assignment that makes the formula true (no green rows).

P is not satisfiable.

The size of the truth table is $2^n$ where $n$ is the number of boolean variables involved.

Hence the problem gets exponentially harder as number of variables increases.