Thinking Cap 2: Search, Theorem Proving and SAT

[Subbarao Kambhampati <rao@asu.edu>]

Just when you thought the cap is gone for good.. Here are some thinking cap questions you can think/comment on: 

1.   If I have n propositions, how many possible clauses are there? (Assume that clauses of the form A V A are automatically simplified to A). Does this help in convincing you that the resolution theoremproving search procedure is *complete* in that it will terminate whether or not  the theorem you are trying to prove actually holds?

2. Suppose you have a propositional knowledge base KB, and you just proved a theorem alpha. Now more facts are added to the KB to give KB'. Will the theorem you proved in KB  still hold in KB'? What if the facts I added made KB' *inconsistent*? [The property we are talking of here is called "Monotonicity"--propositional logic is monotonic.]

2.1.  Question 2 points out that propositional logic is no John Kerry (or Mitt Romney--for you dems)--in that it doesn't "flip-flop". But is not "flip-flopping" really all that great a property? Consider this.  I tell you Tweety is a bird. Do you think Tweety flies?

Now I tell you Tweety is an ostrich. Do you think it flies?  Now I tell you Tweety is a magical ostrich. Do you think it flies? Now I tell you Tweety just got cursed by the local witch/druid. Do you think it flies?   

Do you think it would be good to not "flip-flop" in the example above?

3. The "informedness" of a heuristic is not as great an idea as it is touted to be. You will likely found, during your project 1, that the search with manhattan distance heuristic sometimes does *more* expansions than the search with misplaced tiles

heuristic! In this thinking-cap question you will try to understand why this happens. 

Consider a search problem, for which you have two *admissible* heuristics. h1(n) is h*(n)/5 ;  h2(n) is a constant C (except of course at goal nodes, where it has to be zero), such that h2(n) is always higher than h1(n).  Which is more informed? Which do you think is a better heuristic?

In particular, given a heuristics h2 which is more informed than h2 (in that forall nodes n, h2(n) >= h1(n)), we can only show that the "interior f-contour" nodes expanded by search with h1 are also expanded by h2. 

Specifically, consider a node n' such that f2(n') = g(n') + h2(n') <  f*   (where f*, the optimal cost of the goal node, is the same for both heuristics). So, n' will clearly be expanded by the search with h2. Since h1 <= h2, clearly  f1(n') is also less than f*, and so search with h1 also expands node n'. This shows that the number of nodes on the interior f-contours for h1 can not be fewer than the nodes on the interior f-contours for h1. (An interior f-contour is the set of equi-f-value nodes with  f-values less than f*)

The tricky part is that this subsumption doesn't necessrily hold for nodes that are on the "f* contour"--i.e. nodes that have
f1 or f2 equal to f*. Based on the tie-breaking strategy, a subset of these nodes will likely be expanded before the search terminates. If the subset expanded by h2 is more than that expanded by h1, search with h2 can do more expansions even though it is more informed.

See if you can think of possible reasons why this could happen. [hint: there is a slide in the informed search lecture--with annotation "advanced"--that gives the insights needed, if you are having trouble..]

Rao