156 Chapter 7 Propositional Satisfiability Techniques
rules out the possibility of finding a solution plan of length 6. Davis-Putnam is called
recursively until it discovers that and has to backtrack.
A good choice is instead load(c1,r1,l1,0) because the solution plan of length 6
must first load one of the two robots. Unit propagation does its job by ruling out
all the actions that are not applicable after loading the robot, e.g., load(c1,r1,l1,1).
Some good alternatives to load(c1,r1,l1,0) are load(c2,r2,l1,0) (loading the other
robot as the first action), move(r1,l1,l2,1) (moving the first robot as the second
action), unload(r2,2) (unloading the second robot as the second action), and so
on. Alternative good choices for predicates are loaded(c1,r1,1) ...