Symbolic Reasoning Methods for AI Planning

Abstract

Planning is the act of deliberative thinking before acting. It is based on a symbolic model of the world and the options to act in it, usually defined in function-free first-order logic. The task is to find a sequence of actions (a plan) that leads from a given current state to a desired goal state. The basic, purely physical description may be augmented with a partially ordered grammar-like structure (a Hierarchical Task Network or HTN), which can describe expert knowledge, or practical, legal, or operational requirements. In this talk, I will survey a variety of methods for automatically deriving plans using symbolic methods for planning -- from both my past and future research. These symbolic methods -- in some sense -- translate planning problems into other, simpler symbolic representations and reason over them to find plans. As a basis for these methods, I will firstly introduce relevant theoretical results on planning. First, I will discuss the expressive power of planning formalisms (ECAI'14, ICAPS'16) and second, the computational complexity of HTN planning and related tasks such as HTN plan verification, plan modification, and plan recognition (ICAPS'15, ICAPS'16). Based on these theoretical results, I will develop why SAT-based HTN planning is possible and how it can be implemented. To this end, I will survey several of my publications at top-tier conferences, including papers at ICAPS'17, AAAI'18, AAAI'19, IJCAI'19, AAAI'20, and ICAPS'21 -- in which I developed an highly SAT-based planner for HTN problems including the ability to find optimal plans as well as the grounding as a preprocessing step. Here I will also give an outlook on future developments and new ideas that I propose for SAT-based planning -- including the exploitation of structures in plan (e.g.\ landmarks or operator-counting constraints). Next, I will present the idea of expressing lifted classical planning as SAT (ICAPS'22). The resulting planner LiSAT was the first lifted SAT-based planner -- and proved highly efficient and outperformed all other lifted planners at the time of publication. Notably, LiSAT was the first planner (lifted or grounded) and still is the only one to solve the challenging OrganicSynthesis benchmark -- and could even prove optimality for all plans. I will also outline future ideas to further improve the efficiency of LiSAT. Lastly, I introduce the notion of planning with symbolic symbolic representations (AAAI'21 and ICAPS'23). Here one uses Binary Decision Diagrams to encode large sets of states efficiently. For expressing the additional structure encoded by HTNs, I show how BDDs can be suitably integrated into finite automata. Based on this representation, an efficient and optimal planning algorithm can be derived. Additionally, I show how this algorithm can be extended to also cover oversubscription planning.