Resolution proof compression by splitting
গাণিতিক যুক্তিতে, বিভাজন দ্বারা প্রমাণ সংকোচন একটি অ্যালগরিদম যা রেজোলিউশন প্রমাণের উপর একটি পোস্ট-প্রসেস হিসাবে কাজ করে। স্কট কটন তাঁর গবেষণাপত্র "টু টেকনিকস ফর মিনিমাইজিং রেজোলিউশন প্রুফ"-এ এটি প্রস্তাব করেছিলেন। স্প্লিটিং অ্যালগরিদমটি নিম্নলিখিত পর্যবেক্ষণের উপর ভিত্তি করেঃ অসন্তোষের প্রমাণ এবং একটি পরিবর্তনশীল প্রমাণের পরিপ্রেক্ষিতে, প্রমাণটিকে একটি প্রমাণ এবং একটি প্রমাণ হিসাবে পুনরায় সাজানো (বিভক্ত) সহজ এবং এই দুটি প্রমাণের পুনর্মিলনের (একটি অতিরিক্ত রেজোলিউশন পদক্ষেপ দ্বারা) ফলস্বরূপ মূলটির চেয়ে ছোট প্রমাণ হতে পারে। লক্ষ্য করুন যে একটি পরিবর্তনশীল ব্যবহার করে একটি প্রমাণের মধ্যে বিভাজন প্রয়োগ করা একটি ভিন্ন পরিবর্তনশীল ব্যবহার করে অ্যালগরিদমের পরবর্তী প্রয়োগকে অকার্যকর করে না। প্রকৃতপক্ষে, তুলো দ্বারা প্রস্তাবিত পদ্ধতিটি প্রমাণের একটি ক্রম তৈরি করে, যেখানে প্রতিটি প্রমাণ স্প্লিটিং প্রয়োগের ফলাফল। সিকোয়েন্স নির্মাণের সময়, যদি কোনও প্রমাণ খুব বড় হয়, তবে এটি সবচেয়ে ছোট প্রমাণ হিসাবে সেট করা হয়। একটি ভাল সংকোচন/সময় অনুপাত অর্জনের জন্য, পরিবর্তনশীল নির্বাচনের জন্য একটি অনুসন্ধানমূলক পছন্দসই। এই উদ্দেশ্যে, কটন একটি রেজোলিউশন ধাপের "সংযোজনশীলতা" সংজ্ঞায়িত করে (পূর্ববর্তী এবং সমাধানকারী সহ): তারপর, প্রতিটি চলকের জন্য, এই রেজোলিউশন ধাপগুলির সংখ্যার সাথে পিভট সহ সমস্ত রেজোলিউশন ধাপগুলির সংযোজনশীলতার যোগফল গণনা করা হয়। এইভাবে গণনা করা প্রতিটি স্কোরকে নির্দেশ করে, প্রতিটি চলককে তার স্কোরের আনুপাতিক সম্ভাব্যতা দিয়ে নির্বাচন করা হয়ঃ অসন্তোষের প্রমাণকে প্রমাণ এবং প্রমাণের মধ্যে ভাগ করার জন্য, কটন নিম্নলিখিত প্রস্তাব দেয়ঃ আসুন একটি আক্ষরিককে বোঝাই এবং ধারাগুলির সমাধানকে নির্দেশ করি এবং কোথায় এবং কোথায়। তারপর, এর রেজোলিউশনে নোডের উপর মানচিত্রটি সংজ্ঞায়িত করুনঃ এছাড়াও, খালি ধারাটি হতে দিন। তারপর, এবং যথাক্রমে গণনা এবং দ্বারা প্রাপ্ত হয়। নোটের প্রমাণ তত্ত্ব