Version 1 (modified by ibongartz, 6 days ago) (diff)

First version of wikientry for future work of the SMT Planning Approach.

Future Work

In this wikientry we highlight difficulties of the SMT approach and concrete features which are not working as desired. Next we investigate what possible improvements could be.


Using OMT

Even if the idea of OMT is promising for the RCLL planning task we understand that solving a OMT problem is way more time consuming than a SMT problem. Therefor the complexity of the encoding has to be further decreased or the plan horizon has to be decreased to a value such that OMT becomes possible. But if the plan horizon does not cover the complete plan anymore one has to select subgoals which are manageable in the given plan horizon or maximize some reward which will influence the actions in such a way that eventually the product is constructed.


Due to some restrictions in the clips-executive it is difficult to use all the potential the concurrent plan offers. For example for each wp-put-slide-cc the correct values of rs-before and rs-after have to be specified beforehand. This prohibits the concurrent execution of wp-put-slide-cc actions because the precondition will not be satisfied unless it is the first action in the sequential order.


Re-planning is possible in general but we have to use the original bounded model checking (BMC) approach once we do not longer create a full plan. Moreover we have to omit the inter-action-dependencies because we might have already executed some actions. For the C0 complexity case this is technique is still applicable, but if we have a failure early in some C3 complexity plan re-planning can take a lot of time. First because we omitted the additional constraints reducing solving time greatly and secondly because in the worst case we have to solve ph-1 many formulas with ph the plan horizon we computed for the complete problem.


If we assume that re-planning described above would be feasible in terms of solving time we still have to fix issues regarding robustness. Depending on the time point some robot fails an action and R-1 starts re-planning with the current world state some robots might still be about to execute some actions. Therefor the plan we might obtain is not consistent with the world state in which we want to execute it, possibly leading into a deadlock.

Possible improvements

Apart of the difficulties described above there is plenty of room to improve the SMT planning approach. Some examples are presented in this part of the wikientry.

Produce plan for more than one order

A theoretical strength of the SMT planning approach is that we can describe several goals we desire and then extract a plan which solves all of them. Although it seems unlikely to cover several orders in one formula because each order requires a new set of macro actions it would be a promising feature. Results of the solving procedure could be even that it is not possible to construct all orders in the given time, telling the agent to plan for a different subset of orders.

Use time to get a quasi optimal plan

Using the time variable is a different approach to create better plans. If we assume that our time model is convenient we can activate the time constraint telling that delivery must happen within the delivery window. If the time model is precise an unsatisfiable formula would indicate that no plan solves the given problem. At the same time depending on the delivery window a plan might be better than a plan generated without the time constraints. If the time constraints are activated some plans which would be correct for the formula without the time constraints are not correct in the version with the time constraints. Thus a set of plans are already ruled out without using OMT. Of course the tighter the delivery window is the better the plan will be but at the same time the more unlikely it can be to detect a plan.

Produce plans for all orders and reason about the best order

An alternative would be of course that all combinations of orders are done implicitly by the plugin clips-smt. This is a design decision if the plugin clips-smt is used for goal-reason