💻 computer science

Extending CDCL to disjunctions of parity equations

यह शोध पत्र $\text{CDCL}(\oplus)$ प्रस्तुत करता है, जो XNF सूत्रों के लिए कॉन्फ्लिक्ट-ड्रिवन क्लॉज लर्निंग फ्रेमवर्क का एक सामान्यीकरण है जो पैरिटी रीजनिंग (parity reasoning) का समर्थन करता है और $\text{Res}(\oplus)$ प्रूफ़ सिस्टम का बहुपद रूप से अनुकरण (polynomially simulates) करता है, जो पैरिटी बाधाओं वाले बेंचमार्क पर मौजूदा सॉल्वरों की तुलना में महत्वपूर्ण प्रदर्शन सुधार प्रदर्शित करता है।

मूल लेखक: Paul Beame, Glenn Sun

प्रकाशित 2026-05-15

📖 5 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Paul Beame, Glenn Sun

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप तर्क संबंधी पहेलियों (logic puzzles) की एक विशाल, उलझी हुई गांठ को सुलझाने की कोशिश कर रहे हैं। दशकों से, इन गांठों को सुलझाने के लिए सबसे अच्छा उपकरण एक विधि रही है जिसे CDCL (कॉन्फ्लिक्ट-ड्रिवन क्लॉज लर्निंग) कहा जाता है। CDCL को एक बहुत ही चतुर जासूस के रूप में सोचें जो अनुमान लगाता है, सुरागों का पीछा करता है, और जब वह किसी गतिरोध (विरोधाभास) पर पहुँच जाता है, तो वह अपनी उस गलती से एक मूल्यवान सबक सीखता है ताकि वह दोबारा वही गलती न करे।

हालाँकि, इस जासूस की एक कमज़ोरी है। वह सरल "सही/गलत" (True/False) कथनों वाली पहेलियों को हल करने में उत्कृष्ट है, लेकिन उसे पैरिटी समीकरणों (parity equations)—गणितीय कथनों के बारे में कि वस्तुओं के एक समूह का योग सम (even) है या विषम (odd)—में संघर्ष करना पड़ता है (जैसे यह जाँच करना कि एक बैग में लाल मार्बल्स की संख्या सम है या नहीं)।

यह शोध पत्र एक नए, अपग्रेड किए गए जासूस CDCL(⊕) (उच्चारण "CDCL-पैरिटी") और एक सॉफ़्टवेयर प्रोटोटाइप Xorcle को प्रस्तुत करता है। यह कैसे काम करता है, इसके लिए सरल उपमाओं का उपयोग किया गया है:

1. समस्या: "सम/विषम" की दृष्टि दोष (Blind Spot)

मानक CDCL जासूस ऐसे सुराग देखते हैं जैसे "यदि A सत्य है, तो B को गलत होना चाहिए।" लेकिन कुछ पहेलियाँ ऐसी भाषा में लिखी जाती हैं जैसे "यदि इस समूह में सत्य वस्तुओं की संख्या सम है..."

पुराना तरीका: इन समस्याओं को हल करने के सरल "सही/गलत" सुरागों में अनुवाद करने के पिछले प्रयास किए गए थे। यह एक जटिल 3D मूर्ति का वर्णन केवल 2D छाया बनाकर करने जैसा है। यह काम तो करता है, लेकिन वह चित्र बहुत बड़ा और अस्त-व्यस्त हो जाता है, जिससे जासूस बहुत धीमा हो जाता है।
नया तरीका: CDCL(⊕) "सम/विषम" की भाषा को स्वाभाविक रूप से समझता है। यह सुरागों का अनुवाद नहीं करता; यह उन्हें सीधे समझता है।

2. सुपरपावर: एक उपकरण के रूप में लीनियर अलजेब्रा (Linear Algebra)

जब नया जासूस किसी गतिरोध पर पहुँचता है, तो वह केवल उन विशिष्ट सुरागों को नहीं देखता है जिनके कारण समस्या हुई। वह समीकरणों को मिलाने और जोड़ने के लिए लीनियर अलजेब्रा (गणित की एक शाखा जो समीकरणों से संबंधित है) का उपयोग करता है।

उपमा: कल्पना करें कि आपके पास दो सुराग हैं: "A और B का योग सम है" और "B और C का योग सम है।" एक मानक जासूस यहाँ फंस सकता है। नया जासूस महसूस करता है कि यदि वह इन दोनों सुरागों को जोड़ दे, तो "B" कट जाएगा, जिससे आपको एक बिल्कुल नया, शक्तिशाली सुराग मिलेगा: "A और C का योग सम है।"
यह जासूस को उन पैटर्न और शॉर्टकट देखने की अनुमति देता है जिन्हें पुराना तरीका पूरी तरह से मिस कर देता है।

3. सिद्धांत: यह सिद्ध करना कि जासूस अधिक स्मार्ट है

लेखकों ने केवल एक तेज़ जासूस ही नहीं बनाया; उन्होंने गणितीय रूप से सिद्ध किया कि यह नया जासूस इन प्रकार की पहेलियों के लिए सार्वभौमिक रूप से श्रेष्ठ है।

उन्होंने दिखाया कि CDCL(⊕) किसी भी प्रमाण (proof) का अनुकरण कर सकता है जो "पैरिटी लॉजिक" सिस्टम (जिसे Res(⊕) कहा जाता है) उत्पन्न कर सकता है।
रूपक: यह सिद्ध करने जैसा है कि एक मास्टर शेफ (CDCL(⊕)) उस विशिष्ट ग्रिल (Res(⊕)) द्वारा बनाए जाने वाले हर व्यंजन को बना सकता है जिसे वह ग्रिल बना सकती है, लेकिन वह इसे बहुत तेज़ी से भी कर सकता है यदि उसे कुछ रणनीतिक विकल्प (restarts और decisions) चुनने की अनुमति दी जाए।

4. प्रोटोटाइप: Xorcle

टीम ने इस नए जासूस का एक कामकाजी संस्करण बनाया जिसे Xorcle (XOR और Oracle का मेल) कहा जाता है।

परिणाम: उन्होंने विभिन्न पहेलियों पर वर्तमान सर्वश्रेष्ठ जासूसों (जैसे Kissat और CryptoMiniSAT) के विरुद्ध Xorcle का परीक्षण किया।
- नेटिव पैरिटी पहेलियों पर: Xorcle काफी तेज़ था, जिसने उन समस्याओं को हल किया जिनसे अन्य जासूस जूझ रहे थे या जिन्हें वे समय पर पूरा नहीं कर सके।
- "कठिन" मानक पहेलियों पर: पुराने "सही/गलत" प्रारूप (विशेष रूप से 'Tseitin formulas' नामक एक प्रकार) में लिखी गई पहेलियों पर भी Xorcle आश्चर्यजनक रूप से तेज़ था। जहाँ अन्य जासूसों को घातीय समय (exponential time) लग रहा था (कल्पना कीजिए कि ब्रह्मांड के अंत तक प्रतीक्षा करना), Xorcle ने उन्हें लगभग रैखिक (linear) समय में हल किया (जैसे एक सीधी रेखा पर चलना)।

5. यह कैसे "सोचता" है (मैकेनिज्म)

इसे सफल बनाने के लिए, लेखकों को नए नियम आविष्कार करने पड़े कि जासूस कैसे सीखता है:

समीकरणों पर नज़र रखना: केवल एकल चर (variables) को देखने के बजाय (जैसे "क्या A सत्य है?"), जासूस समीकरणों के पूरे समूहों पर नज़र रखता है।
आधार परिवर्तन (Basis Changes): जब जासूस को किसी गलती से सीखने की आवश्यकता होती है, तो वह केवल एक नया नियम नहीं लिखता। वह समस्या के प्रति अपनी पूरी समझ को पुनर्गठित करता है (आधार बदलना) ताकि ठीक उसी हिस्से को अलग किया जा सके जिसके कारण त्रुटि हुई थी। यह एक मैकेनिक की तरह है जो केवल यह कहने के बजाय कि "इंजन खराब है," इंजन के पुर्जों को पुनर्गठित करता है ताकि यह देख सके कि वास्तव में कौन सा गियर घिसा हुआ है।

सारांश

संक्षेप में, यह शोध पत्र "सम बनाम विषम" गणित वाली तर्क पहेलियों को हल करने का एक नया तरीका प्रस्तुत करता है। इन समीकरणों को स्वाभाविक रूप से समझने के लिए मानक समाधान एल्गोरिदम को अपग्रेड करके, लेखकों ने एक उपकरण (Xorcle) बनाया है जो सैद्धांतिक रूप से सिद्ध रूप से अधिक शक्तिशाली है और अनुभवजन्य रूप से विशिष्ट, कठिन प्रकार की समस्याओं पर वर्तमान अत्याधुनिक सॉल्वर्स की तुलना में बहुत तेज़ है। उन्होंने जासूस की विचार प्रक्रिया को रिकॉर्ड करने का एक नया तरीका (प्रूफ लॉगिंग) भी बनाया है ताकि अन्य लोग समाधान को सत्यापित कर सकें।

तकनीकी सारांश: विच्छेदन (Disjunctions) के लिए CDCL का विस्तार

समस्या विवरण

कॉन्फ्लिक्ट-ड्रिवन क्लॉज लर्निंग (CDCL) SAT सॉल्वर के लिए प्रमुख विधि है, लेकिन यह मौलिक रूप से रेज़ोल्यूशन (Resolution) प्रूफ़ सिस्टम द्वारा सीमित है। वे समस्याएँ जिन्हें रेज़ोल्यूशन में घातांकीय (exponential) प्रूफ़ आकार की आवश्यकता होती है (जैसे कि टेसटीन फॉर्मूला या बायजेक्टिव पिजनहोल सिद्धांत), रेज़ोल्यूशन के लिए सिद्ध रूप से कठिन हैं। जबकि कुछ सॉल्वर अधिक शक्तिशाली प्रूफ़ सिस्टम के अंशों को शामिल करते हैं—जैसे कि कटिंग प्लेन्स का उपयोग करने वाले स्यूडो-बूलियन सॉल्वर या CNF-XOR हैंडल करने वाले CNF-XOR सॉल्वर—ये दृष्टिकोण अक्सर पैरिटी (parity) तर्क को एक अलग मॉड्यूल के रूप में देखते हैं या विशिष्ट सामान्य रूपों (जैसे CNF-XOR) तक ही सीमित रहते हैं।

यह कार्य जिस विशिष्ट अंतर को संबोधित करता है, वह XNF (XOR-OR-AND Normal Form) फॉर्मूलों को सीधे संभालने वाले CDCL-शैली के एल्गोरिदम की कमी है। XNF फॉर्मूले लीनियर क्लॉज़ (linear clauses) के संयोजन (conjunctions) से बने होते हैं, जो पैरिटी समीकरणों का विच्छेदन (disjunction) हैं (उदाहरण के लिए, $(x \oplus y) \lor \neg(y \oplus z)$ )। जबकि Res(⊕) प्रूफ़ सिस्टम (XNF के लिए सामान्यीकृत रेज़ोल्यूशन) कुछ समस्याओं के लिए रेज़ोल्यूशन की तुलना में घातांकीय रूप से अधिक शक्तिशाली है, मौजूदा सॉल्वर CDCL लूप में Res(⊕) तर्क को पूरी तरह से एकीकृत नहीं करते हैं, और न ही वे यह सैद्धांतिक प्रमाण प्रदान करते हैं कि एक CDCL-शैली का एल्गोरिदम Res(⊕) का बहुपद (polynomial) रूप से अनुकरण (simulate) कर सकता है।

कार्यप्रणाली

लेखक CDCL(⊕) का प्रस्ताव करते हैं, जो CDCL एल्गोरिदम का एक सामान्यीकरण है जिसे सीधे XNF फॉर्मूलों पर संचालित करने के लिए डिज़ाइन किया गया है। कार्यप्रणाली तीन मुख्य घटकों पर निर्भर करती है:

Res(⊕) के लिए नए निष्कर्ष नियम (Inference Rules):
लेखक Res(⊕) प्रूफ़ सिस्टम का एक नया लक्षण वर्णन प्रस्तुत करते हैं जो मानक रेज़ोल्यूशन और वीकनिंग (weakening) नियमों के स्थान पर एडिशन (addition) और बेस परिवर्तन (change of basis) का उपयोग करता है।
- एडिशन: $C \lor f$ और $D \lor g$ से, $C \lor D \lor (f + g)$ निकालें।
- बेस परिवर्तन: यदि $C$ , $D$ के समान है ( $C \equiv D$ ), तो $C$ से $D$ निकालें।
  महत्वपूर्ण रूप से, वे एक एफ़ाइन रेज़ोल्यूशन (affine resolution) नियम को परिभाषित करते हैं जहाँ समीकरणों को "आइसोलेट" (isolation) किया जाता है (बेस परिवर्तन के माध्यम से) ताकि एडिशन के माध्यम से रद्दीकरण (cancellation) संभव हो सके। यह वीकनिंग नियम से जुड़े घातांकीय खोज स्थान (search space) की आवश्यकता को समाप्त करता है, जिससे एक बहुपद अनुकरण (polynomial simulation) सक्षम होता है।
लीनियर अलजेब्रा के साथ यूनिट प्रोपेगेशन:
शास्त्रीय CDCL के विपरीत, जो लिटरल असाइनमेंट के आधार पर प्रोपेगेशन करता है, CDCL(⊕) $\mathbb{F}_2$ पर लीनियर अलजेब्रा का उपयोग करके यूनिट प्रोपेगेशन करता है।
- सॉल्वर ज्ञात यूनिट्स (समीकरणों) का एक सेट $U$ बनाए रखता है।
- प्रोपेगेशन यह जाँचता है कि क्या एक लीनियर क्लॉज़ $C$ , $U$ के दिए जाने पर एक नया समीकरण $f$ या विरोधाभास ($1$) को दर्शाता है।
- इसे क्लॉज़ के "लीनियर नेगेशन" (उन असाइनमेंट्स का सबस्पेस जो क्लॉज़ को असत्य बनाते हैं) को $U$ के स्पैन (span) के विरुद्ध कम करके लागू किया जाता है। यदि क्लॉज़ का नेगेशन $U$ के स्पैन और एक एकल समीकरण $f$ के संयोजन के भीतर समाहित है, तो $f$ का निष्कर्ष निकाला जाता है।
कॉन्फ्लिक्ट विश्लेषण के माध्यम से क्लॉज़ लर्निंग:
यह पेपर XNF सेटिंग में 1-UIP (फर्स्ट यूनिक इम्पलीकेशन पॉइंट) क्लॉज़ लर्निंग रणनीति को अनुकूलित करता है। चूंकि इम्पलीकेशन ग्राफ लीनियर समीकरणों में सीधे अनुवादित नहीं होते हैं, इसलिए लर्निंग एल्गोरिदम अर्थ संबंधी (semantically) रूप से कार्य करता है:
- यह कॉन्फ्लिक्ट क्लॉज़ (विरोधाभास का कारण) से शुरू होता है।
- यह सबसे हालिया निर्णय के लिए जिम्मेदार समीकरण को आइसोलेट करने के लिए पुनरावृत्ति से बेस परिवर्तन लागू करता है।
- यह निर्णय वेरिएबल को रद्द करने के लिए आइसोलेट किए गए क्लॉज़ को कॉन्फ्लिक्ट के कारण के साथ जोड़ने के लिए एडिशन नियम लागू करता है।
- यह प्रक्रिया तब तक दोहराई जाती है जब तक कि एक असर्टिंग क्लॉज़ (asserting clause) नहीं मिल जाता (एक ऐसा क्लॉज़ जो वर्तमान निर्णय स्तर पर प्रोपेगेशन को मजबूर करता है)।

मुख्य योगदान

सैद्धांतिक योगदान

द्विदिश संबंध (Bidirectional Connection): पेपर यह सिद्ध करता है कि CDCL(⊕) न केवल Res(⊕) प्रूफ़ बनाता है, बल्कि गैर-नियदार्थिक निर्णयों (nondeterministic decisions) और रीस्टार्ट्स के साथ, Res(⊕) प्रूफ़ सिस्टम का बहुपद अनुकरण (polynomially simulates) भी करता है। यह शास्त्रीय CDCL और रेज़ोल्यूशन के बीच के संबंध को दर्शाता है।
नया प्रूफ़ सिस्टम लक्षण वर्णन: लेखक (addition और change of basis) के एक नए सेट को प्रस्तुत करते हैं जो Res(⊕) के बहुपद रूप से समतुल्य है, लेकिन इसमें वीकनिंग नियम की कमी है, जो इसे एल्गोरिद्मिक कार्यान्वयन के लिए उपयुक्त बनाता है।
इनपुट Res(⊕) समानता: पेपर यह सिद्ध करता है कि CDCL(⊕) में यूनिट प्रोपेगेशन, Res(⊕) के एक खंड (fragment) के समकक्ष है जिसे इनपुट Res(⊕) कहा जाता है, जो शास्त्रीय CDCL के ज्ञात परिणाम का सामान्यीकरण करता है।
सुधारित सिमुलेशन फैक्टर: सिमुलेशन का प्रमाण क्लॉज़ के विखंडन (decompositions) को अवशोषित करने के तरीके को अनुकूलित करके, शास्त्रीय CDCL/रेज़ोल्यूशन संबंध के लिए बहुपद कारक (polynomial factor) में सुधार करता है।

व्यावहारिक योगदान

Xorcle कार्यान्वयन: लेखक XNF के लिए एक प्रूफ-ऑफ-कांसेप्ट सॉल्वर, Xorcle प्रस्तुत करते हैं।
- यह बिट-पैकिंग का उपयोग करके $\mathbb{F}_2$ पर कुशल लीनियर अलजेब्रा को लागू करता है।
- यह CSIDS (क्लॉज़ स्टेट इंडिपेंडेंट डिकेइंग सम) पेश करता है, जो क्लॉज़ चयन के लिए एक नया ह्यूरिस्टिक है जो XNF संदर्भ में VSIDS और CMTF का सामान्यीकरण करता है।
- यह पैरिटी एक्सप्रेशन को सपोर्ट करने के लिए LRUP प्रूफ़ लॉगिंग फॉर्मेट का विस्तार LRUP(⊕) पेश करता है।
XNF के लिए ह्यूरिस्टिक्स: पेपर वॉच्ड स्ट्रक्चर (जटिल वॉचलिस्ट बनाए रखने के बजाय क्लॉज़ के चक्रण), निर्णय प्रक्रियाओं (क्लॉज़ के नेगेशन से रैंडम समीकरणों पर ब्रांचिंग), और फेज सिलेक्शन (क्लॉज़ को असत्य बनाने को प्राथमिकता देना) के अनुकूलन का विवरण देता है।

प्रयोगात्मक परिणाम

लेखकों ने निम्नलिखित बेंचमार्क पर Xorcle का मूल्यांकन किया:

Ascon-128: एक क्रिप्टोग्राफी-संबंधित 2-XNF परिवार।
रैंडम और प्रतिबंधित k-XNFs: विभिन्न वेरिएबल्स और समीकरणों वाले सिंथेटिक फॉर्मूले।
टेसटीन फॉर्मूला (Tseitin Formulas): CNF-एनकोडेड पैरिटी समस्याएँ जो रेज़ोल्यूशन के लिए कठिन मानी जाती हैं।

मुख्य निष्कर्ष:

XNF पर प्रदर्शन: Xorcle ने नेटिव XNF बेंचमार्क पर मौजूदा सॉल्वरों (Kissat, CryptoMiniSat, और 2-Xornado) को पछाड़ दिया। विशेष रूप से, इसने जनरल XNF रीजनिंग का उपयोग करने के बावजूद Ascon-128 इंस्टेंस पर 2-Xornado (एक समर्पित 2-XNF सॉल्वर) से बेहतर प्रदर्शन किया।
टेसटीन फॉर्मूला पर प्रदर्शन: CNF में एनकोडेड टेसटीन फॉर्मूलों पर, Xorcle ने रनिंग टाइम में लगभग बहुपद स्केलिंग (nearly polynomial scaling) प्रदर्शित किया, जबकि रेज़ोल्यूशन-आधारित सॉल्वर को घातांकी समय की आवश्यकता होती है। यह बिना किसी प्रीप्रोसेसिंग के, केवल कोर CDCL(⊕) रीजनिंग पर निर्भर करते हुए प्राप्त किया गया।
निर्णय की गुणवत्ता: Xorcle को प्रतिस्पर्धी सॉल्वरों की तुलना में काफी कम निर्णय लेने की आवश्यकता पड़ी, जो यह सुझाव देता है कि पैरिटी-आधारित ब्रांचिंग और डिडक्शन तंत्र इन समस्या वर्गों के लिए अधिक प्रभावी हैं।

महत्व और दावे

पेपर का दावा है कि CDCL(⊕) पहला कठोर सैद्धांतिक ढांचा और व्यावहारिक कार्यान्वयन प्रदान करता है जो CDCL प्रतिमान में पैरिटी तर्क को पूरी तरह से एकीकृत करता है।

सैद्धांतिक महत्व: यह स्थापित करता है कि CDCL की सीमाएँ एल्गोरिद्मिक संरचना के कारण नहीं, बल्कि अंतर्निहित प्रूफ़ सिस्टम (रेज़ोल्यूशन) के कारण हैं। Res(⊕) में स्थानांतरित होकर, CDCL सैद्धांतिक रूप से उन समस्याओं को हल कर सकता है जो मानक CDCL के लिए घातांकीय रूप से कठिन हैं।
व्यावहारिक महत्व: परिणाम बताते हैं कि नेटिव XNF सॉल्विंग व्यवहार्य है और संभावित रूप से XNF को CNF या CNF-XOR में बदलने से बेहतर है। बिना प्रीप्रोसेसिंग के टेसटीन फॉर्मूला को लगभग बहुपद समय में हल करने की क्षमता, SAT सॉल्विंग में ज्ञात कठिनाई बाधाओं को पार करने के लिए पैरिटी तर्क की क्षमता को उजागर करती है।
भविष्य की दिशाएँ: लेखक विनम्रतापूर्वक नोट करते हैं कि Xorcle एक प्रूफ-ऑफ-कांसेप्ट है। इसमें वर्तमान में कई मानक CDCL अनुकूलन (जैसे क्लॉज़ डिलीशन, उन्नत रीस्टार्ट, डायनेमिक ह्यूरिस्टिक्स) की कमी है और यह अभी तक "1-UIP" या "क्लॉज़ मिनिमाइजेशन" जैसी अवधारणाओं को पूर्णतः सिमेंटिक XNF सेटिंग में सामान्यीकृत नहीं करता है। यह कार्य उन ह्यूरिस्टिक्स के लिए आगे के शोध का द्वार खोलता है जो विशेष रूप से उन CNF फॉर्मूलों को लक्षित करते हैं जिनमें निहित रूप से पैरिटी तर्क की आवश्यकता होती है।