Tomas Balyo

Stephan Gocht

One of the most successful approaches to automated planning is the translation to propositional satisfiability (SAT). This thesis evaluates incremental SAT solving for several modern encodings for SAT based planning. Experiments based on benchmarks from the 2014 International Planning Competition show that an incremental approach significantly outperforms non-incremental solving. Although, planning specific heuristics and advanced scheduling of makespans is not used, it is possible to outperform the state-of-the-art SAT based planning systems Madagascar and PDRPlan in the number of solved instances.