Planning as satisfiability with IPC simple preferences and action costs

摘要

Planning as Satisfiability (SAT) is currently the best approach for optimally (wrt makespan) solving classical planning problems and the extension of this framework to include preferences is nowadays considered the reference approach to compute "optimal" plans in SAT-based planning. It includes reasoning about soft goals and plans length as introduced in the 2006 and 2008 editions of the International Planning Competitions (IPCs). Despite the fact that the planning as satisfiability with preferences framework has helped to enhance the applicability of the SAT-based approach in planning, the actual approach used within the framework somehow suffers from some main limitations: the metrics, i.e. linear optimization functions defined over goals and/or actions, which account for plan quality issues, are fully reduced to SAT formulas, further increasing the size of (often already) big formulas; moreover, the search for optimal solutions is performed by forcing a heuristic ordering. In this paper we address these issues by reducing the IPC planning problems with soft goals (from IPC-5) and/or action costs (from IPC-6) to optimization problems extending SAT and that can naturally handle the integer "weights" of the metrics, i.e. to Max-SAT and Pseudo-Boolean (PB) problems. Our idea is partially motivated by the approach followed by IPPLAN in the deterministic part of the IPC-5 and by the recent availability of efficient Max-SAT and PB solvers. First, we prove that our approach is correct; then, we implement these ideas in SATPLAN and run a wide experimental analysis on planning problems from IPC-5 and IPC-6, taking as references state-of-the-art planners on these competitions and the previous SAT-based approach. Our analysis shows that our approach is competitive and helps to further widen the set of benchmarks that a SAT-based framework can efficiently deal with. At the same time, as a side effect of this analysis, challenging Max-SAT and PB benchmarks have been identified, as well as the Max-SAT and PB solvers performing best on these planning problems.