CSE 573: Homework 2

Due by the start of class, Monday October 30

In this assignment, you will experiment with two different satisifiability solvers: DPLL, a systematic solver, and Walksat, a stochastic solver. Using your own implementation of DPLL and an implementation of Walksat we provide, you will compare the performance of the two solvers on problems of varying difficulty. Finally, we will ask you to try to improve one of the two solvers.

Preliminaries

  1. Kautz and Selman explored the connections among planning, logic and satisifiability in their work, Planning as Satisfiability. Briefly, a solution to a planning problem is specified by a satisfying truth assignment of the conjunction of the axioms describing the plan's initial state, goal state and operators. Time is modeled discretely by integers using predicates that index states by the time at which they hold, and index actions by the time at which they begin. For more details,
  2. Download and install Alchemy, which contains an implementation of Walksat.
  3. Read the manual, doc/manual.pdf, skipping Sections 3.2 & 3.3 if you wish. (In this assignment we'll ignore Markov Logic and subsequently, the weights typically associated with rules)

Part 1: Domain Representation

In this assignment, we will work with the logistics transportation domain, a well-known benchmark domain in planning research. The task of this domain is to transport several objects from their initial location to their desired destinations. The basic elements of the domain are the infrastructure, the transportation units, and the objects. The infrastructure consists of a set of cities, and each city contains a number of locations such as post offices and airports. Trucks and airplanes are the transportation units: trucks can move freely within a city, but transport between cities can only be achieved by airplanes. The basic actions are loading and unloading objects from vehicles, driving trucks and flying airplanes. All actions require one time unit for execution, and any number of non-conflicting actions may occur at the same time step.
  1. Using the predicates defined in logistics.mln, express the following characteristics of the logistics domain in first-order logic. Add these directly to logistics.mln as indicated by the comments. Make each rule a "hard" rule by terminating it with a period.

    1. Objects stay in place or are loaded.
    2. Only load planes/trucks at the same location.
    3. Objects stay in the plane/truck or are unloaded.
    4. Only unload plane/truck at same location.
    5. A plane/truck is always in exactly in one location.
    6. Objects are at at most one location.
    7. Objects are in at most one medium.
    8. Objects are never both at a location and in a medium.
    9. Objects are always somewhere.
    10. A truck is in same city as its location.
    11. An airplane is always at an airport

  2. One of the advantages of formulating a planning problem as satisfiablity is that it makes it easy to supply potentially helpful domain-dependent knowledge to the planner in the form of logical axioms. These axioms can dramatically impact the amount of time it takes a solver to find a solution.

    Using the predicates as in the previous step, express the following statements in first-order-logic. Add these to the bottom of your mln file as well. Comment them out to start; we will explore the impact of adding these heuristics in Part 3.

    1. Once a package leaves a location, it never returns.
    2. A package is never in any city other than its origin or destination cities.
    3. Once a truck is loaded, it should immediately move.
    4. A package never leaves its destination city.

Part 2: Implement DPLL

Implement DPLL. The general flavor of the algorithm is given on page 222 of Russell & Norvig, but you will need to fill in a few details.

It is strongly recommended that you implement the algorithm in C++ as an extension to Alchemy. Read here for advice on implementing DPLL within the Alchemy package.

If you choose to write a standalone version in another language, you may write it in Java, Perl or Python. Regardless, your implementation should be able to handle the same input files as Walksat.

Part 3: Experiment with Walksat and DPLL

Obtain the set of problem instances in the logistics domain. Each file logistics.M.N.db, is the Nth of 5 plans of varying length having M Cities (each with two locations, Airport and Downtown), M Trucks and M Planes. Recall that in the case of planning problems, the database (i.e. the evidence we condition on) is the set of ground atoms describing the initial and goal states.

Empirically compare Walksat and DPLL by running both algorithms on instances from the dataset provided. Using Alchemy, Walksat is called using the infer -m command, using your logistics.mln as the argument to -i and one of the various logistics.M.N.db databases as the argument to -e. Specify At as the query predicate using -q.

For example,

infer -i logistics.mln -e db/logistics.70.3.db -r logistics.70.3.results -q At -o In,MediumAt -m -mwsMaxSteps 100000

Experiment with setting different settings of t using -mwsMaxSteps t where t is the maximum number of steps taken by Walksat.

Begin with only the predicates in rules you wrote in Part 1.1. Next, try adding in the heuristics you wrote in Part 1.2.

In no more than two pages (not including graphs), address the following, numbering the answer to each question:

  1. In graphical form, compare how long it takes each solver to solve problems of varying (1) lengths and (2) difficulties. Summarize your results in a few sentences.
  2. Choose an indentifiable subset of the "hard" instances and run each solver using a series of different time bounds. For each solver, what percent of the problems were able to be solved as a function of the time allowed?
  3. What impact did the various heuristics have on each solver in terms of time and ability to find a solution? Graph the difference in solution time compared to the original, heuristic-free formulation. What combinations did you try? Were some more helpful than others?
  4. Can you conclude anything about simlarities and differences between the problems that are hard for DPLL and those that are hard for Walksat? "Hard" and "easy" should be measured in terms of how long it takes to produce an answer, be it positive or negative, and of the percentage of problems for which the time bounds you set were exceeded.

Part 4: Improve A Sat Solver

Based on your experimental results and your own ideas, propose and implement an improved satisfiability solver for the logistics domain. The goal is to produce a solver that outperforms either (or both!) of DPLL and Walksat in some identifiable subset of the "hard" satisfiability problems. Improvements could be either "internal" (e.g., optimizations to the algorithm that make it run faster) or "external" (e.g., using additional sources of information that allow you to solve the problem better).

You may do this by

In a few paragraphs:

  1. Describe the improvement you made.
  2. Justify your choice and describe what you expect the impact to be.
  3. Show the results of your improved algorithm relative to the results obtained in Part 3. If your novel approach turns out to underperform DPLL and Walksat, propose an empirically-supported explanation of why it didn't work.

What To Turn In

Email the following to Michele by the start of class on Monday, October 30 with the subject title "573 Homework 2"

References

  1. Bayardo, R. and Schrag, R. (1997). Using CSP Look-Back Techniques to Solve Real-World SAT Instances
  2. Moskewicz, et al. (2001). Chaff: Engineering an Efficient SAT Solver.