SAT-Based Planning with Minimal-#actions Plans and “soft” Goals

Planning as Satisfiability (SAT) is the best approach for optimally solving classical planning problems. The SAT-based planner

satplan

has been the winner in the deterministic track for optimal planners in the 4th International Planning Competition (IPC-4) and the co-winner in the last 5th IPC (together with another SAT-based planner). Given a planning problem

Π

,

satplan

works by (

i

) generating a SAT formula

Π

n

with a fixed “makespan”

n

, and (

ii

) checking

Π

n

for satisfiability. The algorithm stops if

Π

n

is satisfiable, and thus a plan has been found, otherwise

n

is increased.

Despite its efficiency, and the optimality of the makespan,

satplan

has significant deficiency related in particular to “plan quality”, e.g., the number of actions in the returned plan, and the possibility to express and reason on “soft” goals.

In this paper, we present

satplan

 ≺ 

, a system, modification of

satplan

, which makes a significant step towards the elimination of

satplan

’s limitations. Given the optimal makespan,

satplan

 ≺ 

returns plans with minimal number of actions and maximal number of satisfied “soft” goals, with respect to both cardinality and subset inclusions. We selected several benchmarks from different domains from all the IPCs: on these benchmarks we show that the plan quality returned by

satplan

 ≺ 

is often significantly higher than the one returned by

satplan

.

Quite surprisingly, this is often achieved without sacrificing efficiency while obtaining results that are competitive with the winning system of the ”SimplePreferences” domain in the satisfying track of the last IPC.