Then for each of these assignments,

we need to check that each of them falsifies at least one clause.

For example, the first one falsifies the first clause.

When x, and y, and z = 0, the first clause is falsified, right?

For the second one, it falsifies the clause y or not z, right?

The third one falsifies the clause x or naught y and so on.

So it can be checked that each of these eight

assignments falsifies at least one clause.

So another way of showing that this formula is satisfiable is the following.

Let's first try to assign the value zero to x.

Then let's take a look at the following clause.

So it is x or not y.

x is already assigned zero.

So the only way to satisfy this clause is to assign the value 0 to y.

So setting x to 0 forces us to set y to 0 also.

Now let's take a look at this clause.

It forces us to set the values 0 to z, also.

But then we see that this clause is already falsified, right,

which tells us that our initial move, I mean to assign 0 to x was a wrong move.

That we need to assign the value 1 to x.

Let's try to do this.

If x = 1, let's take a look at the following clause.

Not x is already falsified in this clause, so we need to assign the value 1 to z.

Now let's take at this clause.

Not z is already falsified here so

we need to assign the value 1 to y.

But then this clause is falsified.

So no matter how we assign x, it forces us to some other assignments and in the end,

we falsify some clause which justifies that this formula is unsatisfiable.

That is a canonical hard problem.

It has applications in various branches of computer science.

In particular because many hard combinatorial problems

are reduced very easily to the satisfiability problems.

I mean, many hard combinatorial problems can be stated very naturally in terms

of SAT and then when a problem is stated in terms of SAT, we can use

a so-called SAT solver, which is a program that solves the satisfiability problem.

There are many such programs and

there is even a [INAUDIBLE] competition of SAT solvers.