6.825: Techniques in Artificial Intelligence
Fall, 2002

Project 1, Part B:

Materials

Notes

(10/3) A new JAR file has been posted. The only difference is that it includes a class techniques.solvers.DPLL that you can use as your SAT solver (though you are encouraged to use your own from part a). This jarfile supercedes the previous one and you should remove PL.jar from your CLASSPATH.

(10/2) Converting from a first-order logic sentence to our FOL grammar (clarification of Figure 3)

Important clarifications:
  1. any time you provide a printout of an assignment, also include a description of it in English (or a with diagram, or something).
  2. if a question asks you to provide an assignment, you do not need to provide _all_ assignments. One will do.
  3. for items 11 and 12, we mean the following:
  4. there is a typo in item 13. the definition of liveness from "formula 8" refers to your revised definition of 'deadlock' from question _10_.
  5. yes, the extra credit is worth actual points on 1b, just as it was on 1a. (note that an "extra credit" problem is distinct from a "bonus challenge!")
  6. yes, please form a group of two (if you like) for this assignment, as well. you can work with the same partner for 3 of the 5 projects.

Answers to some common questions:

  1. "Deadlocked" refers to the whole situation: a situation is deadlocked if both trains can not move. If at least one train has a move available, then we do not consider that situation to be deadlocked.

  2. Your solution to the deadlock questions cannot involve:

  3. Running out of memory:

    you may have gotten "out of memory" errors during the process of changing the FOL sentence into a CNF sentence. this is not a bug in the code, and it's probably not the 'fault' of any individual axiom in your FOL sentence. it's just the nature of exponential growth: converting a sentence from FOL to PL and then to CNF grows exponentially bad with the number of propositions. exponential growth is bad news; if you didn't believe that before, you should now!

    that said, it _is_ possible to do the assignment within the standard memory constraints of the JVM (128 MB). if you are running out of memory, try looking at the following things in your set of axioms:

    there is really no guaranteed method for avoiding memory problems; if you have trouble with it, you'll just need to play around with your sentences until they get small enough.

What to turn in:

Please note that the axioms you come up with should assume as little as possible about the arrangement of rails or number of trains; they should be generally applicable to any world with any number of trains and rails. One of the grading criteria will be the generality of your axioms.
  1. - the formulas 1-6, in the language of figure 3 (hereafter denoted as 'homework language').

  2. - the two new axioms, in the homework language.

  3. - a printout of the found satisfying assignment.
    - in english, a description of the assignment, including the locations of the trains in S1 and S2.

  4. - how you used DPLL to show no crashes (a description of your method)
    - why or why not to use WalkSAT

  5. - the new definition of "legal" in homework language
    - an English or standard FOL description of your new definition
    - any changes to the connects relation?
    - whether the domain is still safe
    - how you used DPLL to show safeness (a description of your method)

  6. - homework language description of layout 2
    - how would you show it is not safe? (describe your method)
    - printout demonstrating safeness (either an assignment, or that your procedure returned 'null' for no assignment)

  7. - the new definition of "legal" in the homework language
    - an English or standard FOL description of your new definition
    - whether the domain is still safe
    - a description of your method for showing that it was still safe
    - a safe configuration you found (or more, if you found more than one) for S1 and S2

  8. - the axiom, in homework language and English/FOL, that asserts that S1 is deadlocked.
    - a description of your method for showing no deadlock in layout 1

  9. - a description of your method for showing deadlock in layout2
    - the members of the ON relation, if your proof method produced an assignment
    - a printout of the assignment, if you have one

  10. - the new axiom for legal (in homework language, and English or FOL)
    - any new axioms or relations that you added
    - a printout of the assignment for the given arrangement

  11. - a description of your method for using SAT to find a connected 2-rail layout that causes deadlock

  12. - a description of your method for using SAT to find that there is no 3-rail layout that causes deadlock

  13. no actual programming is required here. just think about it, and write about what you _would_ do to axiomatize, in FOL, the notion of "eventually moving". then, write about whether the approach of this assignment (i.e. of turning an FOL sentence into a propositional one) would work for proving/disproving the correctness of that condition.

  14. the words "second implication" are a typo: there is only one implication in formula 5. (the formula describing the dynamics.)