28.5. Formula Satisfiability¶
28.5.1. Formula Satisfiability¶
FORMULA SATISFIABILITY PROBLEM (SAT)
1 / 21
Settings
Introduction to Formula Satisfiability
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.
<<<>>>
Introduction to Formula Satisfiability
This slideshow introduces and explains the "Formula Satisfiability" (SAT) Problem.
We start with some definitions and background.
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 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
- $x$
- $\overline{x}$
- T
- F
- F
- T
The AND Operator
- $x$
- $y$
- $x.y$
- T
- T
- T
- T
- F
- F
- F
- T
- F
- F
- F
- F
The OR Operator
- $x$
- $y$
- $x$+$y$
- T
- T
- T
- T
- F
- T
- F
- T
- T
- F
- F
- F
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}$.
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$).
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
- $x_1$
- $x_2$
- $x_3$
- $x_4$
- P
- F
- F
- F
- F
- F
- F
- F
- F
- T
- F
- F
- F
- T
- F
- F
- F
- F
- T
- T
- F
- F
- T
- F
- F
- F
- F
- T
- F
- T
- T
- F
- T
- T
- F
- T
- F
- T
- T
- T
- T
- $x_1$
- $x_2$
- $x_3$
- $x_4$
- P
- T
- F
- F
- F
- F
- T
- F
- F
- T
- F
- T
- F
- T
- F
- F
- T
- F
- T
- T
- T
- T
- T
- F
- F
- F
- T
- T
- F
- T
- F
- T
- T
- T
- F
- T
- T
- T
- T
- T
- T
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
- $x_1$
- $x_2$
- $x_3$
- $x_4$
- P
- F
- F
- F
- F
- F
- F
- F
- F
- T
- F
- F
- F
- T
- F
- F
- F
- F
- T
- T
- F
- F
- T
- F
- F
- F
- F
- T
- F
- T
- F
- F
- T
- T
- F
- F
- F
- T
- T
- T
- F
- $x_1$
- $x_2$
- $x_3$
- $x_4$
- P
- T
- F
- F
- F
- F
- T
- F
- F
- T
- F
- T
- F
- T
- F
- F
- T
- F
- T
- T
- F
- T
- T
- F
- F
- F
- T
- T
- F
- T
- F
- T
- T
- T
- F
- F
- T
- T
- T
- T
- F
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.
Hence the problem gets exponentially harder as number of variables increases.