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

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,
 Read Russell & Norvig, Section 11.5, Planning with Propositional Logic.
 Read the Kautz & Selman paper.
 Download and install Alchemy, which contains an implementation of Walksat.
 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 wellknown 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 nonconflicting actions
may occur at the same time step.
 Using the predicates defined in logistics.mln,
express the following characteristics of the logistics domain in firstorder logic.
Add these directly to logistics.mln as indicated by the comments.
Make each rule a "hard" rule by terminating it with a period.
 Objects stay in place or are loaded.
 Only load planes/trucks at the same location.
 Objects stay in the plane/truck or are unloaded.
 Only unload plane/truck at same location.
 A plane/truck is always in exactly in one location.
 Objects are at at most one location.
 Objects are in at most one medium.
 Objects are never both at a location and in a medium.
 Objects are always somewhere.
 A truck is in same city as its location.
 An airplane is always at an airport
 One of the advantages of formulating a planning problem as satisfiablity is that it makes it easy to
supply potentially helpful domaindependent 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 firstorderlogic.
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.
 Once a package leaves a location, it never returns.
 A package is never in any city other than its origin or destination cities.
 Once a truck is loaded, it should immediately move.
 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:
 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.
 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?
 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, heuristicfree formulation.
What combinations did you try? Were some more helpful than others?
 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
 Adding additional heuristics. They can be general or specific to the logistics domain.
 Implementing an improvement previously reported in relevant literature (see References for ideas)
 Propose your own refinement. A novel solver could be a refinement of DPLL, a refinement of Walksat,
combine elements of both, or incorporate a new approach of your own design.
In a few paragraphs:
 Describe the improvement you made.
 Justify your choice and describe what you expect the impact to be.
 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 empiricallysupported 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"
 Your logistics.mln file from Part 1, which includes the basic domain rules and the four heuristics
 Your implementation of DPLL. If you implemented it as part of Alchemy, please include only the files you changed/added.
 Your analysis from Parts 3 and 4
References
 Bayardo, R. and Schrag, R. (1997). Using CSP LookBack Techniques to Solve RealWorld SAT Instances
 Moskewicz, et al. (2001). Chaff: Engineering an Efficient SAT Solver.