1. Show how to construct a family of CNF formulas for which the "maximize number of satisfied clauses" heuristic used by Walksat is of no help, because the number of unsatisfied clauses is the same in every truth assignment except the solution. By a "family" of clauses, we mean it should be clear from your example how it can be enlarged to use any number of propositions in a non-trivial manner.
2. We say that a CNF formula is Horn iff every clause in it contains at most one positive literal. Suppose you are given an inconsistent formula that is Horn. What is the worst case running time of DPLL on the formula? Why? What is the worst case running time of Walksat? Why?
3. Consider the following two bets, each of which costs $1 to play. In the first bet we run a program which randomly generates a 3-CNF formula containing 1000 propositions where the ratio of clauses to propositions is 4.25. If the formula turns out to be satisfiable, you win $2. In the second bet, I give you a 3-CNF formula containing 1000 propositions where the ratio of clauses to propositions is 3.0. If it turns out to be satisfiable, you win $1,000. Which bet should you take? What are the odds of winning in each case?
4. Consider the "towers of Hanoi" puzzle. (If you don't know what it is, it is described in Wikipedia .) Encode this problem as a STRIPS planning problem for 3 discs. Translate the STRIPS problem into a set of propositional axiom schemas.
5. Specify an algorithm that runs in linear time and determines whether a formula in CNF is valid. DNF is the class of formulas which are disjunctions of conjunctions of literals. What property of a DNF formula can be determined in linear time, and how?
6. Write a formula in FOL that only has models with infinite numbers of individuals. Note that you must write a specific, finite length formula. The formula need NOT be in CNF.
7. Translate the following sentences, as best you can, into FOL:
8. Write a set of FOL axioms that captures the notion of connectivity in a graph. Assume there is a predicate Edge which relates two nodes if there is a edge between them. So, for example, a graph might be specified as follows:
Node(A)
Node(B)
Node(C)
Edge(A,B)
Edge(B,C)
Your axioms for the predicate Connected should be such that Connect(X,Y) is entailed by the specificiation of a graph together with your axioms if and only iff the nodes X and Y are actually connected. For example, in this case
YOUR AXIOMS union EXAMPLE GRAPH |= Connected(A,C)