Assignment 3: Automated Planning

The goal of the assignment is to familiarize with model-based problem solving and specification languages that express transition system models. Planning / sequential decision-making problem is formalized in the NDL language, problem is solved with the Celebes planner, and the solutions are reported as before (NDL specification with comments, output plan, explanation/illustration of the solution plan.)

Obtaining the assignment: The assignment (personal) was emailed to all registered participants. It is also accessible as http://rintanen.info/ASS3/YOURPERSONALSTUDENTID.pdf.

Returning the assignment: Through the Assignments page on MyCourses, as separate files (ndl + PDF or txt file(s)).

Deadline: Thursday March 9, 2017 at 23:55 (for bonus points)

Instructions: The NDL specifications are written with a text editor, and then fed to the Celebes planner by writing e.g.

  ./celebes rushhour.ndl

Celebes will parse and simplify the specification, and then repeatedly call MathSAT to find a plan, and output it. The search strategy is affected by the maximum amount of time allowed: the default is 1800 seconds, and often plans can be found (much) faster by reducing the max time limit, e.g. with the command line option -T 200.

When Celebes finds a plan, it outputs it. Each line of the plan output first contains the "step" of the plan. The steps are numbered from 0 up, and there may be multiple actions at one step (or a step does not necessarily have any actions.) Actions within a step can be ordered arbitrarily, as they are independent (according to the interference condition explained in the lecture.)

MathSAT does not know that the number of actions in a plan should be minimized, so it returns any plan of a given horizon-length that reaches the goals. So the plan may contain unnecessary actions. You force it to find a plan with the minimal horizon length with the option -s 1 (so that horizon length is increased always by 1, not by 5.) This tends to reduce the number of unnecessary actions.

If you encounter problems getting Celebes to solve your problem, you can investigate what happens in Celebes' front end, for example to make sure that some actions or state variables are eliminated because of irrelevance or unreachability (possibly indicating a modeling error.) You can inspect the grounded and simplified specifications by adding the command line option -v 2 (for verbosity level 2). If you want to see the formulas fed to MathSAT, use the command line options -s 3 -t 5 -O to generate .smt files output.{0,1,2,3,4}.smt for horizon lengths 0, 3, 6, 9, 12.

If the planner quickly generates a long sequence of "UNSAT" (for a problem that should have short and simple solutions), there is most likely no solutions, i.e. the goals cannot be reached for some reason (modeling error?). See the planner intermediate results (grounded and simplified actions with -v 2) to see what might be going wrong, or try out simpler goals (with correspondingly simpler plans) to see that things work as expected.

The assignment can be solved with a narrow subset of NDL features. For some of the assignments it is enough to use Boolean state variables, some others benefit from integers. All can be solved without IF-THEN-ELSE statements, but some may benefit from them.

The solutions are not overly complicated: In general, if you think you need very many actions (more than 10) or the actions are getting complicated (several lines, complex constructs, ...), you are probably doing something wrong or in a too complex way. Think about what the essence of the solution is, and try to come with a small number of understandable actions.

Notice: The celebes binary is going to be updated occasionally (bug fixes etc.), so if you encounter problems, please check if there is a new version available. If you encounter bugs, cryptic error messages, other unexplainable behavior, please report so that I can investigate (and fix).

Downloads: celebes (64-binary for Linux March 13 17:17; write "chmod a+x celebes" to make the file executable), NDL documentation (PDF), examples: rushhour.ndl, simpleelevator.ndl , 8puzzle.ndl