Tradeoffs between encodings based on different proof strategies

• Progression (classical frame) encodings lead to higher number of clauses, and allow only serial plans

  • O( #prop * #actions * #levels)
  • To allow parallel plans, we need to look at frame axioms with sets of actions, increasing the clauses exponentially

• Regression (explanatory frame) encodings reduce clauses, and allow parallel plans

  • O( #prop * #levels)

• Empirical results validate dominance of regression over progression encodings

  • The SAT compilation of Graphplan plan-graph corresponds to a form of backward encoding

Previous slide

Next slide

Back to first slide

View graphic version