Cost Optimal Planning as Satisfiability
This work addresses cost-optimal planning for AI systems, but it appears incremental as it builds on existing SAT-based methods with specific bounds.
The paper tackles the problem of computing cost-optimal plans in planning with 0-cost actions by deriving upper bounds on plan length and using them in a SAT-based encoding. The result shows that this approach can compute plans with better costs, often matching the optimal cost, and in some cases proves optimality.
We investigate upper bounds on the length of cost optimal plans that are valid for problems with 0-cost actions. We employ these upper bounds as horizons for a SAT-based encoding of planning with costs. Given an initial upper bound on the cost of the optimal plan, we experimentally show that this SAT-based approach is able to compute plans with better costs, and in many cases it can match the optimal cost. Also, in multiple instances, the approach is successful in proving that a certain cost is the optimal plan cost.