On-Demand Mutex Constraints for Numeric Planning as SMT

Abstract

Planning as Satisfiability Modulo Theories (SMT) has been shown to be a competitive approach for solving numeric planning problems, leveraging the expressiveness of SMT to handle numeric variables and constraints. Being able to set more than one action in a single timestep is crucial for performance, allowing short makespan plans and reducing the number of solver queries required. However, encoding action interference constraints can cause significant formula size blow-up, with mutex constraints dominating the encoding size and limiting scalability. In this paper we present a tool that implements a lazy approach to handling action interference in planning as SMT, exploiting recent developments in solver technology to integrate custom propagators directly into the SMT solver's search process. Rather than eagerly encoding all interference constraints upfront, our propagators add mutex clauses on demand, generating them only when the solver attempts to execute two mutually interfering actions in parallel. Experimental evaluation on standard numeric planning benchmarks demonstrates that our lazy approach is significantly more scalable than the eager approach while maintaining correctness, leading to improved solver performance and making this tool a competitive planner in the numeric setting.