Resolution proof compression by splitting
ریاضیاتی منطق میں، تقسیم کے ذریعے پروف کمپریشن ایک الگورتھم ہے جو ریزولوشن پروف پر عمل کے بعد کے طور پر کام کرتا ہے۔ اسکاٹ کاٹن نے اپنے مقالے "ریزولوشن پروف کو کم سے کم کرنے کی دو تکنیکیں" میں اس کی تجویز پیش کی تھی۔ اسپلٹنگ الگورتھم مندرجہ ذیل مشاہدے پر مبنی ہے: عدم اطمینان اور متغیر کے ثبوت کو دیکھتے ہوئے، ثبوت کو ثبوت اور ثبوت میں دوبارہ ترتیب دینا (تقسیم کرنا) آسان ہے اور ان دونوں ثبوتوں کا دوبارہ امتزاج (ایک اضافی ریزولوشن مرحلے کے ذریعے) اصل سے چھوٹا ثبوت بن سکتا ہے۔ نوٹ کریں کہ متغیر کا استعمال کرتے ہوئے ثبوت میں تقسیم کا اطلاق مختلف متغیر کا استعمال کرتے ہوئے الگورتھم کی مؤخر الذکر درخواست کو کالعدم نہیں کرتا ہے۔ دراصل، کاٹن کی طرف سے تجویز کردہ طریقہ ثبوتوں کا ایک سلسلہ پیدا کرتا ہے، جہاں ہر ثبوت اسپلٹنگ کو لاگو کرنے کا نتیجہ ہوتا ہے۔ ترتیب کی تعمیر کے دوران، اگر کوئی ثبوت بہت بڑا ہوتا ہے، تو اسے سب سے چھوٹا ثبوت مقرر کیا جاتا ہے۔ بہتر کمپریشن/وقت کے تناسب کو حاصل کرنے کے لیے، متغیر انتخاب کے لیے ایک تحقیق مطلوب ہے۔ اس مقصد کے لیے، کاٹن ریزولوشن مرحلے کی "اضطراریت" کی وضاحت کرتا ہے (پیشگی اور حل کے ساتھ): پھر، ہر متغیر کے لیے، ان ریزولوشن مراحل کی تعداد کے ساتھ محور کے ساتھ تمام ریزولوشن مراحل کی اضطراریت کا خلاصہ کرتے ہوئے ایک اسکور کا حساب لگایا جاتا ہے۔ اس طرح سے شمار کیے گئے ہر اسکور کی نشاندہی کرتے ہوئے، ہر متغیر کو اس کے اسکور کے متناسب امکان کے ساتھ منتخب کیا جاتا ہے: عدم اطمینان کے ثبوت کو ثبوت اور ثبوت میں تقسیم کرنے کے لیے، کاٹن مندرجہ ذیل تجویز کرتا ہے: آئیے لفظی کی نشاندہی کریں اور شقوں کے حل کی نشاندہی کریں اور کہاں اور کہاں۔ پھر، ریزولوشن ڈیگ میں نوڈس پر نقشے کی وضاحت کریں: نیز، خالی شق کو اندر آنے دیں۔ پھر، اور بالترتیب کمپیوٹنگ اور کے ذریعے حاصل کیے جاتے ہیں۔ نوٹوں کا ثبوت نظریہ