ساتبلان

Satplan (المعروفة باسم Planning as Satisfiability) هي طريقة للتخطيط الآلي . تقوم بتحويل نموذج مشكلة التخطيط إلى نموذج لمشكلة قابلية الإرضاء المنطقية ، والتي يتم حلها بعد ذلك باستخدام طريقة لتأسيس قابلية الإرضاء مثل خوارزمية DPLL أو WalkSAT .

بالنظر إلى مثال مشكلة في التخطيط، مع حالة أولية معينة، ومجموعة معينة من الإجراءات، وهدف، وطول أفق، يتم إنشاء صيغة بحيث تكون الصيغة قابلة للإشباع إذا وفقط إذا كانت هناك خطة بطول أفق معين. وهذا يشبه محاكاة آلات تورينج مع مشكلة قابلية الإشباع في إثبات نظرية كوك . يمكن العثور على خطة عن طريق اختبار قابلية إشباع الصيغ لأطوال أفق مختلفة. أبسط طريقة للقيام بذلك هي المرور عبر أطوال الأفق بشكل متسلسل، 0، 1، 2، وهكذا.

• مخطط بياني

• HA Kautz و B. Selman (1992). التخطيط كأداة للإشباع. في وقائع المؤتمر الأوروبي العاشر للذكاء الاصطناعي (ECAI'92) ، الصفحات 359-363.
• HA Kautz و B. Selman (1996). دفع الحدود: التخطيط والمنطق القياسي والبحث العشوائي. في وقائع المؤتمر الوطني الثالث عشر للذكاء الاصطناعي (AAAI'96) ، الصفحات 1194-1201.
• ج. رينتانين (2009). التخطيط واختبار القدرة على الإرضاء. في أ. بير، وهـ. فان مارين، وم. هيول، وتوبي والش، محررون، دليل القدرة على الإرضاء ، الصفحات 483-504، مطبعة آي أو إس.