History · Kautz and selman.1992 Inspired by improvements in satisfiabilty algorithms Bia idea Encode planning problem as a(very large) logical formula Initial-state& all-possible-actions goal Find a satisfying assignment to action-time propositions, and we have a plan 16.410/13, Programming SATPlan, Greg SullivanHistory • Kautz and Selman, 1992 • Inspired by improvements in satisfiabity algorithms Big Idea • Encode planning problem as a (very large) logical formula. • Initial-state & all-possible-actions & goal • Find a satisfying assignment to action-time propositions, and we have a plan. Oct. 22, 2003 16.410/13, Programming SATPlan, Greg Sullivan 3