Lesson Plan 9/16/2008
Making local search robust

1. Demonstrate parse-schema-list

2. Demo improving walksat with noise

-- generate large wff at ratio 4
-- solve with walksat -noise 0, explain output
-- solve witih walksat -noise 50: show is much faster

Draw diagram of search space
Talk about escaping from local minima

3. Proof that pure random walk solves 2-SAT

Write on blackboard: pure random walk version of walksat

Draw diagram:  particle moving on a line.  Distance from 0 is Hamming distance
from solution.  Maximum distance is N.

With each step: 1/2 chance of moving toward 0 (solution), 1/2 away.  
But cannot get farther than N away.  Called REFLECTING random walk.

CLAIM: EXPECTED time to solution (hitting 0) is O(N^2).

Let Si = expected time to solution if you start at point i.
CLAIM:
Si = 1 + (S{i-1} + S{i+1})/2

Now let us expand this out for each i, starting with the worst possible one:

Sn = S{n-1} + 1
2S{n-1} = Sn + S{n-1} + 2
...
2S1 = S2 + S0 + 2
S0 = 0

Now add all these together.  Result is

Sn = (2n-1)+(2n-3)+...+3+1 

We look this arithmetic series up in the back of our math book, lo and behold:

Sum = n (start + end)/2 = n ((2n-1) + 1)/2 = n*n

So

Sn = n^2

4. How hard is SAT?  Random wffs give us a handle on this

Variable / Clause ratio == how *constrained* a problem is

With 300 variables:

Generate wff at ratio 6, show it is very easy compared to ratio 4.

Try ratios:  4.1, 4.2
Still SAT?
Try 4.3
Raise -cutoff 10000000    (ten million)

Should run forever.  Try the complete solver satz-rand.

Try diagram.  Label area "provably easy".

Does this same ratio hold true for all *kinds* of wffs?
No: demo on nqueens generator.