تا حالا اسم “circumscription” به گوشت خورده؟ این یه چارچوب منطقی خیلی مهمه که کمک میکنه دانش عمومیِ ما تو منطق رو خیلی راحتتر و منطقیتر روی کامپیوترها پیاده کنیم. خلاصهاش اینه که با circumscription میشه مثلاً تصمیم بگیریم توی یه موقعیت چه چیزی به احتمال زیاد درسته و چه چیزی نه؛ یه جورایی میشه گفت یه مدل برای بستن اطلاعات و پیشفرضهای معقول توی سیستمای مبتنی بر منطق.
دنیای circumscription بدون ابزارهای قوی مثل circ2dlp و aspino اصلاً جذاب نبود! این دوتا نرمافزار معروف، کمک میکنن تا circumscription رو با سرعت و دقت اجرا کنیم و کلیم تو حوزههای جالبی مثل تشخیص خرابی مداری یا همون “model-based diagnosis” (که یعنی پیدا کردن قطعه یا بخش خراب تو یه سیستم بر اساس مدل صحیح اون سیستم) حسابی استفاده میشن.
حالا توی یه کار تحقیقاتی جدید، یه تیم باهوش اومده و با خودش گفته: چرا یه تعریف خفنتر برا این موضوع درست نکنیم؟ اونام چیزی به اسم “مینیمال رداکت” یا همون “کاهش حداقلی” برا circumscription تعریف کردن. کارش چیه؟ یعنی یه راه پیدا کنیم که فقط اون مدلهایی که واقعاً مهم و پایهای هستن رو پیدا کنیم؛ یعنی دیگه بقیه مدلای اضافه و غیرضروری رو بیخیال شیم! جالبتر این که ثابت کردن هر مدل circumscription رو میشه با همین مینیمال رداکت گرفتن.
یه متد جدیدم معرفی کردن به اسم circ-reduct. جریانش اینجوریه که این روش شروع میکنه به گشتن دنبال مدلهای کوچیکتر (یعنی مدلهایی که تعداد فرضیات درستش کمتر باشه یا کمینهتر باشه – یه جورایی “set inclusion” که یعنی مدلهای کوچیکتر از بقیه). هر سری مینیمال رداکت حساب میکنه و با این کار بخشهایی از مسئله رو سادهتر میکنه و بعد دوباره میره سراغ مدل بعدی. این پروسه بارها انجام میشه تا دیگه چیز جدیدی پیدا نشه. یعنی به جای اینکه کل مدلهای ممکن رو بیاره، مینیمالترینها رو پیدا میکنه و از رو اونا بقیه رو حذف میکنه.
خودشون هم ادعا نمیکنن که فقط کشک هستن! کلی تست و آزمایش روی مسائل سخت انجام دادن: مثل تشخیص خرابی مدارات معروف ISCAS85 (که مجموعه معروفی از مدارهای تستیه)، تستای تصادفی روی مسائل CNF (یه قالب استاندارد برای نمایش مسائل منطقی، تقریباً مثل فرمول ریاضی، ولی به زبان منطق)، بعدم مسابقات صنعتی بینالمللی SAT (که رقابت بین نرمافزارهای قدرتمند حلکننده معادلات منطقی هست – SAT solver).
نتیجه چی شد؟
پیدا کردن اینکه این مینیمال رداکت واقعاً باعث شده مدلهای circumscription خیلی سریعتر حساب بشن! مثلاً در مقایسه با circ2dlp که از کلینگو (clingo) استفاده میکنه (اینم یه برنامه خیلی قوی برای حل مسائل منطق جواب-مجموعهایی یا همون ASP یعنی Answer Set Programming)، روش circ-reduct خیلی توی زمان CPU، سریعتر بود.
یه مقایسه دیگه هم با aspino کردن که از یه حلکننده SAT خیلی معروف به اسم glucose و یه تکنیک هوشمندانه به نام “تحلیل هسته ناسازگار” ( Unsatisfiable core analysis یعنی پیدا کردن بخشی از فرضیات که باهم کنار نمیان و باعث غیر قابل حل شدن مسئله میشن) استفاده میکنه. برای مسائل تصادفی و مسائل استاندارد صنعتی، باز هم circ-reduct سریعتر بود. هرچند روی مسائل تشخیص مدار، سرعتش تقریباً مشابه aspino بود اما کمتر عقب میموند.
در کل، داستان اینه: با استفاده از مینیمال رداکت میشه مدلهای circumscription رو هم دقیقتر، هم سریعتر و با دردسر کمتر حساب کرد. اگه تو کار هوش مصنوعی یا منطق و سیستمای تشخیص خرابی هستی، احتمالاً این خبر میتونه مسیری جدید و باحال جلوم بذاره!
منبع: +
