Accelerating SAT Based Planning with Incremental SAT Solving

One of the most successful approaches to automated planning is the translation to propositional satisfiability (SA T). We employ incremental SA T solving to increase the capabilities of several modern encodings for SA T based planning. Experiments based on benchmarks from the 2014 International Planning Competition show that an incremental approach significantly outperforms non incremental solving. Although we are using sequential scheduling of makespans, we can outperform the state-of-the-art SA T based planning system Madagascar in the number of solved instances.