
Title:
09ps06 Satisfaction Guaranteed Solution

Description:

Alright, first if we had a complete series of snapshots

from a nondeterministic RAM solving SAT on his formula.

Well, a nondeterministic RAM can solve SAT in polynomial time,

so we can check those in polynomial time as well

since we just have a list of these.

So once we have those, we can definitely verify that his formula is satisfiable.

Now if we had a list of satisfiable clauses,

this actually isn't enough to verify that Bob's formula is also satisfiable.

To see this, let's take a look at the formula in somewhat pythonic form,

X and not X.

Now clearly X is a satisfiable clause and so is not X,

but the entire Boolean formula is definitely not satisfiable.

So a list of satisfiable clauses actually isn't enough

for us to believe Bob.

Now if we had a satisfying assignment for all of the variables in the formula,

then sure, we can just plug them into the formula

and check on a deterministic RAM,

and that occurs in polynomial time.

Similarly, if add all calls to if_better on the Boolean formula,

well, if_better is the only difference

between a nondeterministic and a deterministic RAM,

so if we had all the calls to if_better,

we wouldn't actually have to simulate if_better,

we would know what the algorithm did at each step of the process.

So we could also check Bob's formula using just this.

Not even a complete series of snapshots is necessary

just the calls to if_better.

Now let's say we had a satisfying assignment for 90% of the variables.

Well, 90% of the variables still leaves 10%,

and 10% of exponential is, well, exponential.

So we would still have exponentially many variables to check.

So this actually doesn't work.