And it is already clear, so if the formula is satisfiable,

this means that for each clause we can select one literal

such that the resulting set of literals is consistent.

But this also means that from each of these five block, so

this is the first block, corresponding to the first block, this is the second,

this is the third one, this is the fourth one, this is the fifth one.

We can select exactly the same vertex that corresponds to the selected

literal in this formula.

So if the formula is satisfiable, then in each block we can select on vertex.

And we know that they are not going to be joined by edges,

because vertices from different blocks are only joined if they are complementary.

And we know that our set of literals does not contain complimentary literals.

So if the formula is satisfiable,

then this graph contains an independent set of size 5.

And vice versa uses graph contents an independent set of size 5 and

the formula is satisfied both.

Why is that?

Well just because any independent set of size 5

has exactly 1 various of nature of these blocks.

And we know that the labels of these vertices give us a set of

literals which is consistent, which doesn't contain

a literal together with it's complementary literal.

So it gives us a set of literals such that it

intersects every clause of our initial formula.

Which means that if the response,

they are satisfying the assignment of the initial formula.

To summarize, let's state this reduction formally.

The reduction works as follows, given formula F in 3-CNF, that is

a collection of clauses, each of length at most three, what is the following?

We scan the set of the clauses from left to right and

for each clause, we introduce three or two,

or just one dependent on the number of literals in this clause.

Three or two, or one vertices, and we'll label them with

literals of this clause and we join every two of them by an edge.

So we are now constructing a graph G, and

this forces every independent set in this graph to contain

at most one vertex from each block to responding to a single clause.