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: x1,x2,x3
We use Boolean operators AND (+) , OR (.), and NOT (¯ over a variable), which follow these truth tables:
The NOT Operator
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: x1+x2.¯x3
A literal is either a boolean variable (x) or its negation (¯x)
For example: a,¯b,¯g,c,¯c.
A clause is a disjunction (OR) of literals such as l1+l2+l3+⋯+ln for literals li.
For example: (a+¯b) , ¯g , (c+¯f+¯e+h).
A Conjunctive normal form (CNF) is a conjunction (AND) of clauses.
For example: ¯x1.(x1+x2).(x3+x4+¯x5).(x1+x3).(¯x3+x2+¯x5).(x1+x2+¯x3).(x3+x4+¯x2).(¯x4+¯x1+¯x5).(x1+x3+x5)
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: (x1+x2.x3) is "True" for x1=T , x2=T, x3=T , hence satisfiable.
(x1.¯x1) is always "False", hence not satisfiable.
Given any boolean formula in CNF, is the formula satisfiable?
P = (x1 + x2).(x2 + ¯x3 + x4).(x1 + ¯x2 + x3 + x4).(¯x1 + x3)
Truth Table for P
- x1
- x2
- x3
- x4
- 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
- x1
- x2
- x3
- x4
- 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 = (x1 + x2).(x2 + ¯x3 + x4).(x3 + ¯x4).(x1 + ¯x1).(x1 + ¯x2 + x3 + x4)
Truth Table for P
- x1
- x2
- x3
- x4
- 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
- x1
- x2
- x3
- x4
- 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 2n where n is the number of boolean variables involved.
Hence the problem gets exponentially harder as number of variables increases.