برنامه ریزی کلاسیک به صورت ارضای بولی

برنامه ریزی کلاسیک به صورت ارضای بولی

در پست قبلی دیدید که الگوریتم SATPLAN چگونه مسئله های برنامه ریزی را که به زبان منطق مرتبه اول بیان شدند، حل میکند. در این جا نشان می دهیم که چگونه می توان توصیف PDDL را به شکلی ترجمه کرد که توسط SATPLAN قابل پردازش باشد. این ترجمه در چندین مرحله آسان صورت می گیرد.

ترجمه به مسئله ارضای بولی SAT، یکی از معروفترین و موثرترین روشهای خودکار برنامه ریزی کلاسیک می باشد که توصیف آن این گونه است:

 

♦ فعالیت ها را بصورت گزاره بنویسید:

هر جای هر شمای فعالیت، مجموعه ای از فعالیت های پایه ای را قرار دهید که این فعالیت های پایه ای با جایگزینی ثوابت به جای متغیرها به دست آمده اند. این فعالیت های پایه ای بخشی از ترجمه نیستند، اما در مراحل بعدی استفاده خواهند شد.

 

♦ حالت شروع را تعریف کنید:

F⁰ را برای هر fluent مثل F در حالت شروع مسئله و ¬Fرا برای هر fluent که در حالت شروع اشاره نشدند، اثبات کنید.

 

♦ هدف را به صورت گزاره بنویسید :

برای هر متغیر موجود در هدف، لیترال هایی را که شامل این متغیر است، با ترکیب فصلی روی ثوابت جایگزین کنید.

 

♦ اصول حالت پسین successor – state axioms را اضافه کنید :

برای هر fluent مثل F یم اصل موضوعی به صورت زیر اضافه کنید:

F^t+1  ↔ ActionCausesF^t  V  (F^t ᴧ  ¬ActionCausesNot F^t)

که ActionCausesF ترکیب فصلی تمام فعالیت های پایه ای است که F در لیست افزودنی  آنها وجود دارد و ActionCausesNot F ترکیب فصلی تمام فعالیت های پایه ای است که F در لیست حذف آنها وجود دارد.

 

♦ اصول موضوعی پیش شرط را اضافه کنید :

برای هر فعالیت پایه ای A، اصل موضوعی  A^t → PRE(A)^t را اضافه کنید، یعنی اگر فعالیتی در زمان t انجام شود، آنگاه پیش شرط ها باید درست بوده باشند.

 

♦ اصل منبع فعالیت را اضافه کنید :

فرض کنید هر فعالیت از فعالیت دیگر متمایز است.

 

ترجمه حاصل به شکلی است که می توانیم آن را به SATPLAN تحویل دهیم تا جوابی را پیدا کند.