The resurgence of propositional satisfiability in AI planning

A natural approach to classical AI planning is to treat it as a logical deduction problem. That is, with states and actions expressed in the language of formal logic, and the existence of a solution being equivalent to the satisfiability of logical formulae. An early example is McCarthy’s situation calculus published in 1963.

Attempts to use general theorem solvers on these formulations proved impractical, however. It was thought that in order to make progress specialised algorithms would have to be employed, and these remained the focus of research for a long time (Weld 1999).

The mid-90s saw the publication of Graphplan, a specialised algorithm with unprecedented performance. However it was also around this time that SATPlan (based on satisfiability) emerged as a competitive planner. By the end of the decade this had evolved into Blackbox — and absorbed Graphplan’s magic along the way!

Graphplan

From the mid-70s to the mid-90s, the research landscape was dominated by partial order planning (Norvig and Russell, p. 394). Blum and Furst (1995) changed that with their publication of Graphplan, which was orders of magnitude faster than anything seen before.

The innovation at its heart is the construction of a planning graph — hence the name. The levels in the graph represent the steps of a plan. Each level contains the fluents and actions that could appear at that step. Also recorded are mutual exclusions, or mutexes. These are fluents or actions which can’t happen together and thus constrain the eventual solution.

The planning graph can be built in polynomial time, and serves as a simplified formulation of the problem. Graphplan goes on to extract a solution by performing a regression (backwards) search on the graph.

SATPlan

By this time, high-performance solvers existed for propositional satisfiability (SAT) problems. Futhermore, they were being actively worked on and improved year on year by the research community.

When Kautz and Selman (1992) first started to leverage these general solvers for planning, the results were unremarkable (Weld 1999). However it wasn’t long before SATPlan started to make waves. By 1996, Kautz and Selman had demonstrated that it was orders of magnitude faster than Graphplan on certain ‘tricky’ problems.

The performance of this approach was so impressive, in fact, that it actually motivated researchers to explore other NP-hard computational problems to which planning might be translated (Rintanen and Hoffmann 2001).

Blackbox

In 1999, Kautz & Selman published Blackbox. The key insight was that a planning graph did the best job of simplifying a problem, whilst SAT solvers were quickest at extracting a solution.

So Blackbox’s first move is to construct a planning graph. It then converts the graph to a SAT problem, encoding the mutexes as extra clauses in the formula. Finally it employs a state-of-the-art theorem solver to extract the solution.

The resulting algorithm outperformed both Graphplan and SATPlan alone, and set new benchmarks against challenging planning problems.

Conclusion

When SAT planning was first rekindled in the early 90s it showed some promise. However, specialised algorithms still dominated AI planning. Researchers faced the challenge of finding an efficient translation of planning problems into logical formulae.

Graphplan was a revolutionary specialised algorithm. But above and beyond this its planning graph proved to be a powerful vehicle for encoding problems into the SAT formulation.

Blackbox’s combination of these technologies made it a formidable AI planner.

References

Blum, A. L. and Furst, M. L., 1995. Fast Planning Through Planning Graph Analysis. Proceedings of IJCAI-95, pp. 1636–1642, Montreal.

Kautz, H. A. and Selman, B., 1992. Planning as Satisfiability. ECAI, vol. 92, pp. 359–363.

Kautz, H. A. and Selman, B., 1996. Pushing the envelope: Planning, propositional logic, and stochastic search. Proceedings of the National Conference on Artificial Intelligence, pp. 1194–1201.

Kautz, H. A. and Selman, B., 1999. Unifying SAT-based and graph-based planning. IJCAI, vol. 99, pp. 318–325.

McCarthy, J., 1963. Situations, actions, and causal laws. Stanford Artificial Intelligence Project, Memo №2.

Norvig, P. and Russell S. J., 2016. Artificial Intelligence: A Modern Approach, 3rd ed., Pearson Education Limited, Harlow.

Rintanen, J. and Hoffmann, J., 2001. An overview of recent algorithms for AI planning. KI, 15(2), pp. 5–11.

Weld, D. S., 1999. Recent advances in AI planning. AI magazine, 20(2), p. 93.