
Title:
Preprocessing For SAT  Intro to Theoretical Computer Science

Description:

So let's have a look. What about x1? So here we have x1, not x1, not x1 and x1.

I have no idea what to do with that, so it's probably not easy.

What about x2? So here we have x2, x2, not x2, still kind of difficult to see if we should set it to false,

making this clause here satisfied or if we should set it to true, satisfying those two clauses up here.

It's not easy, or at least it's not doable without playing around with other true or false assignment.

What about x3, same case? So here we have x3, not x3, x3, again, x3, not x3, no idea what to do with that.

So all that remains is x4. Now, where does x4 appear? X4 appears here and x4 appears here.

And what you'll notice is that both time we have not x4. So x4 could appear in two forms, right?

So x4 could appear as x4, or as not x4. But we have just this one form appearing.

And this goes back to the answer of the previous quiz, where I gave you an intuition for what makes SAT hard.

What makes SAT hard is that, if you choose a truth assignment of true or false, then some clauses obviously

become satisfied, but in other clauses you get less variables to satisfy that clause.

However, if you have a variable that just appears in one form, then you don't have that dilemma.

It's always clear that we should set x4, which is the correct answer here, to false, because then we satisfy this clause here,

we satisfy this clause here, but there are no secondary effects again. So all of the other clauses are unaffected by

how we set x4. So we just choose it to our advantage. And of course, also, this is something that is easy to do algorithmically.

So for each of the variables that appear in a Boolean formula, an algorithm could just go through

and see if that variable appears in both formsso as the variable itself and in the "not" form.

And if it appears just in one form, then we already know how to set it. So we have now found a third preprocessing rule for SAT.

Now, let's step back a little bit and look at the general requirements of preprocessing.