Planning as Satisfiability for Cyber-Physical Systems Francesco Leofante ? University of Genoa, Genoa, Italy RWTH Aachen University, Aachen, Germany Abstract. Planning as Satisfiability is one of the most well-known and effective techniques for classical planning. The basic idea is to encode the existence of a plan with n steps as a propositional satisfiability formula obtained by unfolding, n + 1 times, the symbolic transition relation of the automaton described by the planning problem. Planning for Cyber- Physical Systems, however, requires languages that are more expressive than propositional logic to model, e.g., energy consumption, time du- rations. We study how first-order (arithmetic) theories can be used to this end, and propose to leverage recent advances in Satisfiability Mod- ulo Theories solving to compute optimal plans for complex systems that require both propositional and numeric reasoning. 1 Introduction In planning, the objective is to find a sequence of actions that leads a system from a given initial state to a goal state. As shown by Kautz and Selman for the first time in [6], classical planning problems can be naturally formulated as propositional satisfiability problems and solved efficiently by SAT solvers. The idea is to encode the existence of a plan of a fixed length n as the satisfiability of a propositional logic formula: the formula for a given n is satisfiable if and only if there is a plan of length n leading from the initial state to the goal state, and a model for the formula represents such plan. Classical planning abstracts aways from numeric quantities, however these are of paramount importance when dealing with a Cyber-Physical System (CPS). Consider a robot managing orders in a smart warehouse. Once a new order request arrives, the robot would take the order, fetch the requested product and prepare it for delivery. With an increasing number of orders, large teams of robots would be needed to keep the business running. Each robot in the team would have to come up with an efficient plan to deliver its order, all while considering what other robots do so as to avoid interferences. On top of this, optimality targets such as minimizing overall energy consumption or time to delivery, should be taken into account to ensure efficiency. The natural encoding of planning problems for domains like the one we just introduced requires an extension of propositional logic with arithmetic theories, ? Joint work with Erika Ábrahám and Armando Tacchella. such as the theory of reals or integers. Advances in satisfiability checking led to powerful Satisfiability Modulo Theories (SMT ) solvers such as [3, 12], which can be used to check the satisfiability of first-order logic formulas expressed over arithmetic theories and thus model numeric quantities such as the ones mentioned above. For the synthesis of optimal plans we need to go beyond satisfiability and resort to optimization: an optimal plan is a satisfying solution for the logical formula encoding the planning problem, which ensures optimality of a desired objective function that defines a relevant cost metric. The importance of solving such optimization problems has been recognized by the SMT community [2, 17, 19] and led to the emergence of a new field called Optimization Modulo Theories (OMT ) and the development of efficient OMT solvers [1, 21]. In our work we intend to leverage recent advances in satisfiability checking to extend the original Planning as Satisfiability framework to enable optimization over reward structures expressed in first-order arithmetic theories. More specifi- cally, we propose to reduce optimal numeric planning to OMT: combining sym- bolic reachability techniques and optimization, OMT solvers can be leveraged to generate optimal plans for complex systems that require both propositional and numeric reasoning. In the following we discuss our experience using OMT decision procedures for planning. After briefly presenting the preliminaries on which this work builds, we present our results on optimal planning in a smart logistic domain involving multi-robot systems. We then briefly sketch our ongoing work and then con- clude with future directions we intend to explore to further the development of planning as OMT. 2 Preliminaries 2.1 Satisfiability Modulo Theories and optimization Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some decidable theory T . In particular, SMT generalizes Boolean satisfiability (SAT) [4] by adding background theories such as the theory of real numbers, integers, and the theories of data structures. To decide the satisfiability of an input formula ϕ in CNF, SMT solvers such as [12, 3] typically proceed as follows. First a Boolean abstraction abs(ϕ) of ϕ is built by replacing each constraint by a fresh Boolean proposition. A SAT solver searches for a satisfying assignment S for abs(ϕ). If no such assignment exists then the input formula ϕ is unsatisfiable. Otherwise, the consistency of the as- signment in the underlying theory is checked by a theory solver. If the constraints are consistent then a satisfying solution (model ) is found for ϕ. Otherwise, the theory solver returns a theory lemma ϕE giving an explanation for the conflict, e.g., the negated conjunction of some inconsistent input constraints. The expla- nation is used to refine the Boolean abstraction abs(ϕ) to abs(ϕ)∧abs(ϕE ). These steps are iteratively executed until either a theory-consistent Boolean assignment is found, or no more Boolean satisfying assignments exist. Standard decision procedures for SMT have been extended with optimization capabilities, leading to Optimization Modulo Theories (OMT). OMT extends SMT solving with optimization procedures to find a variable assignment that defines an optimal value for an objective function f (or a combination of multiple objective functions) under all models of a formula ϕ. As noted in [20], OMT solvers such as [21, 1] typically implement a linear search scheme, which can be summarized as follows. Let ϕS be the conjunction of all theory constraints that are true under S and the negation of those that are false under S. A local optimum µ for f is computed 1 under the side condition ϕS and ϕ is updated as ^ ϕ := ϕ ∧ (f ./ µ) ∧ ¬ ϕS , ./∈ {<, >} Repeating this procedure until the formula becomes unsatisfiable will lead to an assignment minimizing f under all models of ϕ. 2.2 Planning Modulo Theories Planning as Satisfiability frames the existence of a plan of a fixed length p as the satisfiability of a propositional logic formula: the formula for a given p is satisfiable if and only if there is a plan of length p leading from the initial state to the goal state, and a model for the formula represents such plan. Standard reductions of classical planning to SAT abstract away from numeric quantities, however this is not the case for SMT. More precisely, Planning Modulo Theories can be formalized as follows. World states are described using an ordered set of real-valued variables x = {x1 , . . . , xn }. We also use the vector notation x = (x1 , . . . , xn ) and write x0 and xi for (x01 , . . . , x0n ) and (x1,i , . . . , xn,i ) respectively. We use special variables A ∈ x to encode the action to be executed at each step and t ∈ x for the associated time stamp. A state s = (v1 , . . . , vn ) ∈ Rn specifies a real value vi ∈ R for each variable xi ∈ x. The planning domain can then be represented symbolically by mixed-integer arithmetic formulas defining the initial states I(x), the transition relation T (x, x0 ) (where x describes the state before the transition and x0 the state after it) and a set of final states F (x). The transition relation is defined in terms of actions that can be performed at each step. A plan of length p is a sequence s0 , . . . , sp of states such that I(s0 ) and T (si , si+1 ) hold for all i = 0, . . . , p − 1, and F (sp ) holds. Thus, plans are models for the formula:     ^ _ I(x0 ) ∧  T (xi , xi+1 ) ∧  F (xi ) (1) 0≤i