Resolution proof compression by splitting
गणितीय तर्क में, विभाजन द्वारा प्रमाण संपीड़न एक एल्गोरिथ्म है जो संकल्प प्रमाणों पर प्रक्रिया के बाद के रूप में काम करता है। स्कॉट कॉटन ने अपने पेपर "टू टेक्निक्स फॉर मिनिमाइज़िंग रिज़ॉल्यूशन प्रूफ" में इसका प्रस्ताव रखा था। विभाजन एल्गोरिथ्म निम्नलिखित अवलोकन पर आधारित हैः असंतोषजनकता और एक चर के प्रमाण को देखते हुए, प्रमाण को एक प्रमाण और एक प्रमाण में फिर से व्यवस्थित (विभाजित) करना आसान है और इन दो प्रमाणों के पुनर्संयोजन (एक अतिरिक्त संकल्प चरण द्वारा) के परिणामस्वरूप मूल से छोटा प्रमाण हो सकता है। ध्यान दें कि एक चर का उपयोग करके एक प्रमाण में विभाजन लागू करना एक भिन्न चर का उपयोग करके एल्गोरिथ्म के बाद के अनुप्रयोग को अमान्य नहीं करता है। वास्तव में, कपास द्वारा प्रस्तावित विधि प्रमाणों का एक क्रम उत्पन्न करती है, जहाँ प्रत्येक प्रमाण स्प्लिटिंग को लागू करने का परिणाम होता है। अनुक्रम के निर्माण के दौरान, यदि कोई प्रमाण बहुत बड़ा होता है, तो उसे सबसे छोटा प्रमाण माना जाता है। एक बेहतर संपीड़न/समय अनुपात प्राप्त करने के लिए, परिवर्तनीय चयन के लिए एक शोध वांछनीय है। इस उद्देश्य के लिए, कपास एक संकल्प चरण की "योगात्मकता" को परिभाषित करता है (पूर्ववर्ती और संकल्पक के साथ): फिर, प्रत्येक चर के लिए, इन संकल्प चरणों की संख्या के साथ धुरी के साथ सभी संकल्प चरणों की योगात्मकता को जोड़ते हुए एक अंक की गणना की जाती है। इस तरह से गणना किए गए प्रत्येक अंक को निरूपित करते हुए, प्रत्येक चर को उसके अंक के आनुपातिक संभावना के साथ चुना जाता हैः असंतोष के प्रमाण को प्रमाण और प्रमाण में विभाजित करने के लिए, कपास निम्नलिखित का प्रस्ताव करता हैः आइए एक शाब्दिक को निरूपित करें और खंडों के समाधान को निरूपित करें और कहाँ और कहाँ। फिर, के रिज़ॉल्यूशन डैग में नोड्स पर मानचित्र को परिभाषित करेंः इसके अलावा, खाली खंड होने दें। फिर, और क्रमशः गणना और द्वारा प्राप्त किए जाते हैं। नोट्स सबूत सिद्धांत