[Script Info]
Title:
[Events]
Format: Layer, Start, End, Style, Name, MarginL, MarginR, MarginV, Effect, Text
Dialogue: 0,0:00:00.00,0:00:02.00,Default,,0000,0000,0000,,Let's say we have a friend Bob.
Dialogue: 0,0:00:02.00,0:00:05.00,Default,,0000,0000,0000,,Bob is blue, he's had a nasty run in with a can of paint.
Dialogue: 0,0:00:05.00,0:00:07.00,Default,,0000,0000,0000,,Now let's assume that Bob has a Boolean formula,
Dialogue: 0,0:00:07.00,0:00:11.00,Default,,0000,0000,0000,,not necessarily this one but just some Boolean formula.
Dialogue: 0,0:00:11.00,0:00:13.00,Default,,0000,0000,0000,,And suppose Bob comes to us and tells us I've already
Dialogue: 0,0:00:13.00,0:00:16.00,Default,,0000,0000,0000,,found out that this Boolean formula is satisfiable.
Dialogue: 0,0:00:16.00,0:00:19.00,Default,,0000,0000,0000,,Now let's say we don't necessarily trust Bob.
Dialogue: 0,0:00:19.00,0:00:22.00,Default,,0000,0000,0000,,Bob is given to exaggeration.
Dialogue: 0,0:00:22.00,0:00:26.00,Default,,0000,0000,0000,,We'd like to be able to figure out in polynomial time
Dialogue: 0,0:00:26.00,0:00:29.00,Default,,0000,0000,0000,,whether or not Bob is telling us the truth.
Dialogue: 0,0:00:29.00,0:00:31.00,Default,,0000,0000,0000,,So how would be go about doing that?
Dialogue: 0,0:00:31.00,0:00:34.00,Default,,0000,0000,0000,,Let's say Bob came to us with a complete series of snapshots
Dialogue: 0,0:00:34.00,0:00:38.00,Default,,0000,0000,0000,,from a nondeterministic RAM solving SAT on his formula.
Dialogue: 0,0:00:38.00,0:00:44.00,Default,,0000,0000,0000,,Would that be enough for us to believe that he had a satisfiable formula?
Dialogue: 0,0:00:44.00,0:00:48.00,Default,,0000,0000,0000,,How about if he had a list of satisfiable clauses?
Dialogue: 0,0:00:48.00,0:00:53.00,Default,,0000,0000,0000,,For example, he had a list that had x as the satisfiable clause
Dialogue: 0,0:00:53.00,0:00:56.00,Default,,0000,0000,0000,,and not Y as a satisfiable clause.
Dialogue: 0,0:00:56.00,0:00:59.00,Default,,0000,0000,0000,,Then for the entire Boolean formula,
Dialogue: 0,0:00:59.00,0:01:03.00,Default,,0000,0000,0000,,could we then determine whether it was satisfiable or not?
Dialogue: 0,0:01:03.00,0:01:05.00,Default,,0000,0000,0000,,What about if you had a satisfying assignment for all
Dialogue: 0,0:01:05.00,0:01:07.00,Default,,0000,0000,0000,,of the variables in the formula?
Dialogue: 0,0:01:07.00,0:01:11.00,Default,,0000,0000,0000,,What if we had all the calls to if_better on the Boolean formula?
Dialogue: 0,0:01:11.00,0:01:15.00,Default,,0000,0000,0000,,So not necessarily a complete series of snapshots
Dialogue: 0,0:01:15.00,0:01:18.00,Default,,0000,0000,0000,,from a nondeterministic RAM solving SAT on his formula,
Dialogue: 0,0:01:18.00,0:01:20.00,Default,,0000,0000,0000,,but just all the calls to if_better.
Dialogue: 0,0:01:20.00,0:01:23.00,Default,,0000,0000,0000,,Would that be enough for us to believe Bob?
Dialogue: 0,0:01:23.00,0:01:25.00,Default,,0000,0000,0000,,And finally, what if we had a satisfying assignment
Dialogue: 0,0:01:25.00,0:01:29.00,Default,,0000,0000,0000,,for not all the variables but 90% of the variables in Bob's formula.
Dialogue: 0,0:01:29.00,0:01:31.00,Default,,0000,0000,0000,,Could we believe him then?
Dialogue: 0,0:01:31.00,9:59:59.99,Default,,0000,0000,0000,,Please check all that apply.