6.7. 3-CNF Satisfiability¶

6.7.1. 3-CNF Satisfiability (3-SAT)¶

1 / 18 Settings

<<<>>>

Introduction to 3-CNF Satisfiability

This slideshow introduces and explains the "3-CNF Satisfiability" (3-SAT) Problem.

We start with some definitions and background.

A 3-CNF is a Boolean formula that is an AND of clauses, each of which is an OR of
exactly 3 distinct literals.

Example of 3-CNF: $(x_1 + x_2 + x_3).(\overline{x_1} + x_4 + x_6).(x_2 + \overline{x_5}+ \overline{x_3}).(x_1 + \overline{x_3} + \overline{x_6})$.

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 3-CNF is said to be satisfiable if it has a satisfying assignment.

Given some boolean formula in CNF such that each clause has exactly 3 literals, is the formula satisfiable?

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

Truth Table for P

$x_1$
$x_2$
$x_3$
$x_4$
P

$x_1$
$x_2$
$x_3$
$x_4$
P

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

P is satisfiable.

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

Truth Table for P

$x_1$
$x_2$
$x_3$
$x_4$
P

$x_1$
$x_2$
$x_3$
$x_4$
P

There exists no 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 the number of variables increases.

Saving...

Server Error
Resubmit

Try out an instance of the 3-SAT problem on your own.

Senior Algorithms

Chapter 6 Limits to Computing

6.7. 3-CNF Satisfiability¶

6.7.1. 3-CNF Satisfiability (3-SAT)¶