💻 computer science

Computing Short SAT Implicants via Ising/QUBO Encodings

यह शोध पत्र एक नवीन आइसिंग/QUBO एनकोडिंग फ्रेमवर्क प्रस्तुत करता है जो "डोंट-केयर" (don't-care) सिमेंटिक्स को शामिल करने के लिए द्वैध-ध्रुवीयता प्रतिनिधित्व (dual-polarity representation) का उपयोग करता है, जिससे ग्राउंड स्टेट रिट्रीवल के माध्यम से लघु आंशिक संतुष्ट असाइनमेंट (इम्प्लिकेंट्स) की कुशल गणना और उनका न्यूनीकरण सक्षम होता है।

मूल लेखक: Giuseppe Spallitta, Leonardo Duenas-Osorio, Moshe Y. Vardi

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

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

CC BY 4.0

मूल लेखक: Giuseppe Spallitta, Leonardo Duenas-Osorio, Moshe Y. Vardi

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

कल्पना कीजिए कि आप एक विशाल, जटिल पहेली को हल करने की कोशिश कर रहे हैं। कंप्यूटर लॉजिक (जिसे SAT कहा जाता है) की दुनिया में, लक्ष्य आमतौर पर यह खोजना होता है कि सभी टुकड़ों को एक साथ कैसे फिट किया जाए ताकि तस्वीर समझ में आ सके। पारंपरिक रूप से, कंप्यूटर इस काम को करने के लिए पहेली के हर एक टुकड़े को भर देता है, भले ही वे टुकड़े अंतिम तस्वीर के लिए वास्तव में महत्वपूर्ण न हों। वे आपको एक "पूर्ण" समाधान देते हैं जहाँ हर वेरिएबल या तो "चालू" (On) होता है या "बंद" (Off)।

लेकिन अक्सर, आपको पूरी तस्वीर की आवश्यकता नहीं होती है। आपको बस कुछ मुख्य टुकड़ों की आवश्यकता होती है जो यह सिद्ध कर सकें कि पहेली काम करती है। शायद आप जानना चाहते हैं कि कोई सिस्टम क्यों विफल हुआ, या आप समाधानों की एक विशाल सूची को एक छोटे, आसानी से पढ़े जाने वाले सारांश में संकुचित करना चाहते हैं। इन मामलों में, आपको एक "आंशिक" (partial) समाधान चाहिए होता है: कुछ टुकड़े "चालू" या "बंद" के रूप में सेट होते हैं, जबकि बाकी को खाली छोड़ दिया जाता है, जैसे कि एक "परवाह नहीं" (Don't Care) का संकेत।

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

नया "परवाह नहीं" (Don't Care) वाला तरीका

लेखकों ने इन कठोर रोबोटों को चीजें खाली छोड़ना सिखाने के लिए एक चतुर तरीका ईजाद किया है। उन्होंने यह किया प्रत्येक पहेली के टुकड़े को एक के बजाय दो चेहरे देकर।

एक मानक वेरिएबल की कल्पना करें जो एक लाइट स्विच की तरह है जो या तो चालू (ON) है या बंद (OFF) है।
लेखकों की नई विधि हर वेरिएबल को दो स्विच देती है:

एक "पॉजिटिव" स्विच (चालू के लिए)।
एक "नेगेटिव" स्विच (बंद के लिए)।

यहाँ जादू है:

यदि पॉजिटिव स्विच चालू है, तो वेरिएबल सत्य (True) है।
यदि नेगेटिव स्विच चालू है, तो वेरिएबल असत्य (False) है।
यदि दोनों स्विच बंद हैं, तो वह अनिर्धारित (Unassigned) है (एक "परवाह नहीं" या Don't Care स्थिति)।
यदि दोनों स्विच चालू हैं, तो यह एक गलती है (वर्जित है)।

इस "दोहरे-स्विच" सिस्टम का उपयोग करके, कंप्यूटर अब "दोनों स्विच बंद" करके स्वाभाविक रूप से एक "परवाह नहीं" (Don't Care) स्थिति को दर्शा सकता है।

"ऊर्जा" का खेल

कंप्यूटर इन पहेलियों को हल करने के लिए सबसे कम "ऊर्जा" (energy) वाली स्थिति खोजने की कोशिश करता है (जैसे एक गेंद ढलान के सबसे निचले बिंदु की ओर लुढ़कती है)। लेखकों ने खेल के नियम इस प्रकार बनाए हैं कि:

नियमों का पालन होना चाहिए: यदि कोई पहेली का नियम (clause) टूट जाता है, तो ऊर्जा बहुत अधिक बढ़ जाती है। कंप्यूटर को इससे बचना ही होगा।
सरलता को पुरस्कृत किया जाता है: लेखकों ने एक नियम जोड़ा है कि, "हर बार जब आप एक स्विच चालू करते हैं, तो आप एक छोटा शुल्क (fee) देते हैं।"

चूंकि कंप्यूटर सबसे कम कुल ऊर्जा चाहता है, इसलिए वह सभी नियमों का पालन करते हुए और कम से कम स्विच चालू करते हुए काम करेगा। वह स्वाभाविक रूप से अनावश्यक स्विचों को "दोनों बंद" (Don' Don't Care) की स्थिति में छोड़ देगा।

संकुचन (Shrinking) और ध्यान केंद्रित करना (Focusing)

लेखक इस ट्रिक का उपयोग करने के दो मुख्य तरीके दिखाते हैं:

संकुचन (Shrinking): कल्पना कीजिए कि आपके पास पहले से ही एक पूर्ण समाधान (सभी स्विच चालू या बंद) है। आप इस नए तरीके का उपयोग इसे "सिकुड़ने" के लिए कर सकते हैं। आप कंप्यूटर को बताते हैं, "उन स्विचों को रखें जो पहले से ही चालू हैं, लेकिन नियमों को तोड़े बिना उनमें से जितने संभव हो सके उतने स्विच बंद करने का प्रयास करें।" कंप्यूटर अतिरिक्त स्विचों को हटा देगा, जिससे आपको उन स्विचों का सबसे छोटा समूह मिलेगा जो अभी भी पहेली को हल करता है।
फोकसिंग (प्रोजेक्शन - Projection): कभी-कभी, आप वेरिएबल्स के एक विशिष्ट समूह (जैसे "दृश्यमान" टुकड़े) के बारे में ही परवाह करते हैं, जबकि अन्य केवल छिपे हुए समर्थन के रूप में होते हैं। लेखक यह बताने का तरीका दिखाते हैं कि कंप्यूटर को कैसे कहें: "केवल दृश्यमान स्विचों को चालू करने के लिए शुल्क लें। छिपे हुए स्विच जो भी होने चाहिए, वे हो सकते हैं।" यह कंप्यूटर को केवल महत्वपूर्ण वेरिएबल्स का उपयोग करके सबसे संक्षिप्त स्पष्टीकरण खोजने के लिए मजबूर करता है।

उन्होंने क्या पाया

लेखकों ने यादृच्छिक पहेलियों और जटिल सूत्रों पर इस विचार का परीक्षण किया। उन्होंने पाया कि:

कंप्यूटर ने सफलतापूर्वक ऐसे समाधान खोजे जहाँ लगभग एक-तिहाई वेरिएबल्स को खाली (अनिर्धारित) छोड़ा गया था, जिससे यह सिद्ध हुआ कि पहेली अभी भी काम करती है।
कंप्यूटर को एक लूप में चलाकर (एक समाधान खोजना, फिर उसे फिर से सिकोड़ने का प्रयास करना), वे लगभग हमेशा सबसे छोटा संभव समाधान पा सकते थे।
यह विधि तब भी अच्छी तरह काम करती है जब पहेली को एक अलग प्रारूप में बदला जाता है (जैसे एक जटिल वाक्य को सरल नियमों की सूची में बदलना), जब तक कि "छिपे हुए" समर्थन वेरिएबल्स को सही ढंग से माना जाए।

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

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

तकनीकी सारांश: Ising/QUBO एन्कोडिंग के माध्यम से लघु SAT इम्पलिकेंट्स (Implicants) की गणना

1. समस्या विवरण

व्याख्या (explanation), निदान (diagnosis), और मॉडल संपीड़न (model compression) सहित कई तर्क कार्यों (reasoning tasks) में, पूर्ण असाइनमेंट (total assignments) के बजाय लघु आंशिक संतुष्ट असाइनमेंट (short partial satisfying assignments/implicants) की आवश्यकता होती है। इन संदर्भों में, अनअसाइंड (unassigned) चर वास्तविक "डोंट-केयर" (don't-cares) के रूप में कार्य करते हैं, और अक्सर चरों का एक उपसमूह (दृश्य चर/visible variables) ही अर्थपूर्ण रूप से प्रासंगिक होता है, जबकि अन्य छिपे हुए समर्थन (hidden support) के रूप में कार्य करते हैं।

जबकि आधुनिक SAT सॉल्वर कुशल रूप से पूर्ण संतुष्ट असाइनमेंट की गणना करते हैं, लघु इम्पलिकेंट्स प्राप्त करने के लिए आमतौर पर बार-बार SAT कॉल या समर्पित पोस्ट-प्रोसेसिंग की आवश्यकता होती है। इसी तरह, मानक SAT-to-Ising/QUBO फॉर्मुलेशन स्वाभाविक रूप से सीमित हैं: वे CNF फॉर्मूला को द्विघात ऊर्जा फलनों (quadratic energy functions) में मैप करते हैं जहाँ ग्राउंड स्टेट्स (ground states) पूर्ण असाइनमेंट के अनुरूप होते हैं। Ising/QUBO मॉडल प्रत्येक स्पिन को एक मान देता है, जिसमें "अनअसाइंड" चरों के लिए कोई मूल प्रतिनिधित्व नहीं होता है। फलस्वरूप, लघु इम्पलिकेंट्स की गणना ऐतिहासिक रूप से स्वयं द्विघात अनुकूलन मॉडल के भीतर कैप्चर होने के बजाय बाहरी एल्गोरिदम द्वारा छोड़ी गई है।

2. कार्यप्रणाली (Methodology)

लेखक एक एकीकृत अनुकूलन ढांचा प्रस्तावित करते हैं जो द्विघात Ising/QUBO मॉडल के भीतर तीन-मूल्य वाले आंशिक असाइनमेंट (True, False, Unassigned) को स्वाभाविक रूप से सपोर्ट करता है।

2.1 द्वैत-ध्रुवीयता प्रतिनिधित्व (Dual-Polarity Representation)

अनअसाइंड चरों का प्रतिनिधित्व करने के लिए, ढांचा एक द्वैत-ध्रुवीयता एन्कोडिंग (dual-polarity encoding) पेश करता है। प्रत्येक प्रपोज़िशनल वेरिएबल $A_i$ के लिए, दो बाइनरी स्पिन $(p_i, n_i)$ का उपयोग किया जाता है:

$(1, 0) \implies A_i = \top$ (True)
$(0, 1) \implies A_i = \bot$ (False)
$(0, 0) \implies A_i$ अनअसाइंड है (don't-care)
$(1, 1) \implies$ असंगत (Inconsistent/Forbidden)

एक सिमेंटिक कंसिस्टेंसी पेनल्टी $M \cdot p_i n_i$ को असंगत अवस्था को वर्जित करने के लिए जोड़ा जाता है।

2.2 क्लॉज एन्कोडिंग (Clause Encoding)

क्लॉज को मानक द्विघात पेनल्टी फलनों का उपयोग करके एन्कोड किया जाता है। एक क्लॉज $C_k = (\ell_1 \lor \ell_2 \lor \ell_3)$ के लिए, लिटरल्स को उनके संबंधित पोलैरिटी स्पिनों पर मैप किया जाता है। द्विघात रूप बनाए रखने के लिए, एक ऑक्सिलरी वेरिएबल $c_k$ पेश किया जाता है जो उस स्थिति को कैप्चर करता है जहाँ पहले दो लिटरल्स 'फॉल्स' होते हैं। ऊर्जा फलन उन कॉन्फ़िगरेशन को दंडित करता है जहाँ सभी लिटरल्स 'फॉल्स' होते हैं (अर्थात, उनके संबंधित सभी स्पिन 0 होते हैं)।

2.3 स्पर्सिटी और ऑब्जेक्टिव फंक्शन (Sparsity and Objective Function)

ऊर्जा फलन में एक स्पर्सिटी टर्म जोड़ा जाता है: $E_{sparse} = \gamma \sum (p_i + n_i)$ । यह टर्म सक्रिय स्पिनों को दंडित करता है, जिससे ऑप्टिमाइज़र कम चरों वाले कॉन्फ़िगरेशन (लघु इम्पलिकेंट्स) की ओर झुकता है।
कुल ऊर्जा फलन है:
$E_F = \sum M p_i n_i + \sum E_{clause}(k) + \gamma \sum (p_i + n_i)$

2.4 वेट रिजीम्स (Weight Regimes)

पेपर शुद्धता सुनिश्चित करने के लिए वेट्स ( $\lambda$ क्लॉज पेनल्टी के लिए, $M$ कंसिस्टेंसी के लिए, $\gamma$ स्पर्सिटी के लिए) पर सैद्धांतिक स्थितियाँ स्थापित करता है। विशेष रूप से, यदि $\lambda > n\gamma$ और $M > n\gamma$ (जहाँ $n$ चरों की संख्या है), तो ऊर्जा फलन के ग्राउंड स्टेट्स सटीक रूप से न्यूनतम-कार्डिनैलिटी इम्पलिकेंट्स (minimum-cardinality implicants) के अनुरूप होते हैं।

2.5 श्रिंकिंग और प्रोजेक्शन (Shrinking and Projection)

इम्पलिकेंट श्रिंकिंग (Implicant Shrinking): एक पूर्ण संतुष्ट असाइनमेंट दिए जाने पर, ढांचा "विपरीत" पोलैरिटी स्पिनों को 0 पर फिक्स करके सर्च स्पेस को प्रतिबंधित करता है। यह ऑप्टिमाइज़र को मौजूदा असाइनमेंट से लिटरल्स को हटाने की अनुमति देता है, जिससे एक वैध इम्पलिकेंट के रूप में सबसे छोटा उप-असाइनमेंट मिलता है।
प्रोजेक्शन (Projection): दृश्य चरों (visible variables) के एक उपसमूह $P$ पर ध्यान केंद्रित करने के लिए, स्पर्सिटी पेनल्टी केवल $P$ के चरों पर लागू की जाती है। छिपे हुए चर $H$ , स्पर्सिटी द्वारा अनकन्स्ट्रेंड रहते हैं, जो मुक्त सहायक समर्थन (free auxiliary support) के रूप में कार्य करते हैं। यह मॉडल को $P$ पर लघु असाइनमेंट खोजने की अनुमति देता है जबकि $H$ के माध्यम से फॉर्मूला को संतुष्ट किया जाता है।

3. मुख्य योगदान (Key Contributions)

नेटिव थ्री-वैल्यूड एन्कोडिंग: एक SAT-to-Ising/QUBO एन्कोडिंग जो द्वैत-ध्रुवीयता सिमेंटिक्स के माध्यम से आंशिक असाइनमेंट (True/False/Unassigned) को स्वाभाविक रूप से प्रदर्शित करती है, जिससे "अनअसाइंड" अवस्थाओं की व्याख्या के लिए बाहरी पोस्ट-प्रोसेसिंग की आवश्यकता समाप्त हो जाती है।
लचीले ऑब्जेक्टिव वेरिएंट्स: QUBO फॉर्मुलेशन जहाँ इम्पलिकेंट श्रिंकिंग को पोलैरिटी प्रतिबंधों द्वारा और प्रोजेक्शन को दृश्य चरों पर स्पर्सिटी पेनल्टी को प्रतिबंधित करके प्राप्त किया जाता है, जो एक ही निश्चित द्विघात मॉडल संरचना के भीतर काम करता है।
सैद्धांतिक गारंटी: विशिष्ट वेट रिजीम्स ( $\lambda > n\gamma, M > n\gamma$ ) की पहचान जो यह गारंटी देते हैं कि ग्राउंड स्टेट्स न्यूनतम-कार्डिनैलिटी इम्पलिकेंट्स के अनुरूप हैं। पेपर अंतिम ऊर्जा मान से सीधे वैध इम्पलिकेंट्स को पहचानने के लिए एक मानदंड प्रदान करता है।
अनुभवजन्य सत्यापन (Empirical Validation): रैंडम 3-SAT और नॉन-CNF फॉर्मूला पर सिम्युलेटेड एनीलिंग का उपयोग करके मूल्यांकन, जो लघु आंशिक असाइनमेंट बनाने और पुनरावृत्ति (iterative refinement) के माध्यम से लघुता (minimality) प्राप्त करने की एन्कोडिंग की क्षमता को प्रदर्शित करता है।

4. प्रयोगात्मक परिणाम (Experimental Results)

लेखकों ने दो बेंचमार्क सेट पर सिम्युलेटेड एनीलिंग (SA) का उपयोग करके अपने एन्कोडिंग का मूल्यांकन किया:

Random 3-SAT: कम क्लॉज-टू-वेरिएबल डेंसिटी ( $m/n = 1.5$ ) वाले संतुष्ट उदाहरण।
Non-CNF Formulas: Tseitin/Plaisted-Greenbaum रूपांतरणों के माध्यम से CNF में परिवर्तित किए गए बूलियन फॉर्मूला, जो छिपे हुए सहायक चरों के साथ एक प्रोजेक्टेड सेटिंग बनाते हैं।

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

कॉम्पैक्टनेस (Compactness): रैंडम 3-SAT पर, एन्कोडिंग औसतन लगभग एक-तिहाई चरों को अनअसाइंड छोड़ देती है और संतुष्टि (satisfiability) को बनाए रखती है।
लघुता (Minimality): जबकि बेसलाइन SA छोटे-से-मध्यम इंस्टेंस पर न्यूनतम-कार्डिनलिटी असाइनमेंट पाता है, समस्या का आकार बढ़ने पर सफलता दर कम हो जाती है (लोकल मिनिमा के कारण)। हालांकि, इटरेटिव रिफाइनमेंट (सर्वश्रेष्ठ समाधान को फ्रीज करना और और अधिक श्रिंक करने के लिए SA को फिर से चलाना) परिणामों में काफी सुधार करता है।
Minimality बनाम Minimum-Cardinality: इटरेटिव रिफाइनमेंट उच्च संभावना के साथ इनक्लूजन-मिनिमलिटी (प्राइम इम्पलिकेंट्स) प्राप्त करता है। Minimum-cardinality (ग्लोबल मिनिमम साइज) प्राप्त करना कठिन है लेकिन अक्सर देखा जाता है, विशेष रूप से नॉन-CNF बेंचमार्क में जहाँ संरचना यूनिफॉर्म कंप्लीशन की अनुमति देती है।
प्रोजेक्टेड सेटिंग: प्रोजेक्टेड मोड में, विधि दृश्य चरों पर न्यूनतम-कार्डिनलिटी असाइनमेंट को सफलतापूर्वक रिकवर करती है, भले ही कुल चरों का उच्च अनुपात (65–70%) छिपे हुए सहायक चर हों।

5. महत्व और दावे (Significance and Claims)

यह पेपर दावा करता है कि यह ढांचा लघु आंशिक असाइनमेंट कंप्यूट करने के लिए एक एकीकृत अनुकूलन दृष्टिकोण प्रदान करता है, जो AllSAT या एक्सप्लेनेशन पाइपलाइनों में श्रिंकिंग सबरूटीन की आवश्यकता को बदल देता है।

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