الگوریتم برنامه ریزی گزاره ای SATPLAN
الگوریتم برنامه ریزی گزاره ای SATPLAN
در این الگوریتم چگونگی ساخت برنامه ریزی با استنتاج منطقی را بررسی میکنیم. ایده ی اصلی بسیار ساده است:
1- جمله ای بسازید که شامل موارد زیر باشد:
► Init0 ، کلکسیونی از ادعا ها راجع به حالت شروع.
Transitiont ,…, Transition1 ► ، "اصول حالت پسین" برای تمام فعالیت های ممکن در هر زمان تا زمان ماکزیمم t.
► ادعاهایی که مشخص میکند در زمان t به هدف میرسیم.
2- کل جمله را به حل کننده SAT ارائه دهید. اگر حل کننده یک مدل ارضاپذیر را بیابد، آنگاه هدف قابل دسترس است، اگر جمله ارضاپذیر نباشد، آنگاه مسئله ی برنامه ریزی غیرممکن است.
3- با فرض اینکه مدلی پیدا شود، متغیرهایی را که نشان دهنده فعالیت هستند و مقدار آنها true است، از مدل استخراج کنید. آنها با هم برنامه ریزی دست یابی به هدف را نشان میدهند.
رویه برنامه ریزی گزاره ای SATPLAN ، که شبه کد آنرا در ادامه می بینید، ایده ی مطرح شده را با یک تغییر نشان میدهد. چون عامل نمیداند چند مرحله باید طی کند تا به هدف برسد، الگوریتم، هر تعداد ممکن از مراحل (t) را تست میکند تا به حداکثر طول ممکن برنامه ریزی، یعنی Tmax برسد. در این روش تضمین میشود که کوتاه ترین برنامه ریزی در صورت وجود پیدا شود. با توجه به روش جست وجوی SATPLAN برای جواب، این روش نمیتواند در محیط "پاره ای قابل مشاهده" استفاده شود. SATPLAN مقادیری را به مجموعه ای از متغیرهای غیرقابل مشاهده نسبت میدهد که برای تولید جواب، مهم هستند.
مرحله کلیدی در استفاده از SATPLAN ، ساخت پایگاه دانش است. ممکن است در بازرسی سببی، به نظر برسد که اصول موضوعی کافی باشد. اما، بین نیازمندی های ایجاب منطقی و نیازمندی های ارضاپذیر ، تفاوت عمده ای وجود دارد.
SATPLAN یک ابزار اشکال زدایی خوب برای پایگاه های دانش است، زیرا مکان هایی را که دانش از دست داده اند، مشخص میکند.
SATPLAN جنبه های جالب دیگری نیز دارد. اولی این است که مدل هایی با فعالیت های غیرممکن را می یابد. برای عدم تولید برنامه ریزی هایی با فعالیت های نامعتبر، باید اصول پیش شرط را اضافه کنیم که میگوید برای انجام این فعالیت باید پیش شرط های آن برآورده شوند.
نکته جالب دوم درباره SATPLAN، ایجاد برنامه ریزی با استفاده از چندین فعالیت بطور همزمان است. برای برطرف کردن این مشکل اصل منبع فعالیت را معرفی میکنیم.
بطور خلاصه، SATPLAN مدل هایی را برای جمله حاوی، حالت شروع، هدفف اصل حالت پسین، اصل پیش شرط، و اصل منبع فعالیت پیدا میکند. میتوان نشان داد که این کلکسیون از اصول موضوعی، کافی است، به این معنا که دیگر جوابهای ساختگی وجود ندارد. هر مدلی که این جمله ی گزاره را ارضا میکند، یک برنامه ریزی معتبر برای مسئله اصلی خواهد بود.
شبه کد الگوریتم جست وجوی SATPLAN
در این الگوریتم، مسئله برنامه ریزی به یک جمله CNF ترجمه میشود که در آن، هدف در مرحله زمانی ثابت t اثبات میشود و اصل موضوعی مربوط به هر مرحله ی زمانی تا t نیز گنجانده میشوند. اگر الگوریتم ارضاپذیری، مدلی را بیابد، آنگاه با توجه به نمادهای گزاره ای که به فعالیت ها مراجعه میکنند و مقدار آنها در مدل برابر true است، یک برنامه ریزی استخراج میشود. اگر هیچ مدلی وجود نداشته باشد آنگاه این فرآیند تکرار میشود به طوری که هدف به مرحله بعدی منتقل میشود.
function SATPLAN(init, transition, goal, Tmax) returns solution or failure
inputs : init , transition, gold, constiture a description of the problem
Tmax , an upper limit for plan lemgth
for t = 0 to Tmax do
cnf <-- TRANSLATE-TO-SAT(init, transition, goal, t)
model <-- SAT-SOLVER(cnf)
if model is not null then
return EXTARCT-SOLUTION(model)
return failure
