💻 computer science

A SAT-Based Exact Approach for Radio k-Labeling

यह शोध पत्र रेडियो $k$ -लेबलिंग समस्या के लिए एक सटीक, वृद्धिशील (incremental) SAT-आधारित ढांचे को प्रस्तुत करता है जो 38 उदाहरणों के लिए नए सर्वश्रेष्ठ-ज्ञात समाधान स्थापित करके और 146 बेंचमार्क ग्राफों में से 109 के लिए इष्टतमता (optimality) को प्रमाणित करके अत्याधुनिक वाणिज्यिक सॉल्वरों और ह्यूरिस्टिक्स से बेहतर प्रदर्शन करता है।

मूल लेखक: Huong Vu Thanh, Duc Dao Van, Khanh To Van

प्रकाशित 2026-07-23

📖 4 मिनट में पढ़ें☕ कॉफ़ी ब्रेक में पढ़ें

CC BY 4.0

मूल लेखक: Huong Vu Thanh, Duc Dao Van, Khanh To Van

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

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

लंबे समय से, गणितज्ञ इस पहेली को हल करने की कोशिश कर रहे हैं। कुछ लोगों ने चतुर शॉर्टकट (heuristics) बनाए हैं जो जल्दी से एक अच्छा उत्तर का अनुमान लगा लेते हैं, लेकिन वे यह साबित नहीं कर सकते कि वह सबसे अच्छा उत्तर है। अन्य लोगों ने शक्तिशाली कंप्यूटर प्रोग्रामों (जैसे ILP सॉल्वर) का उपयोग करने की कोशिश की है ताकि सटीक समाधान पाया जा सके, लेकिन ये प्रोग्राम अक्सर बहुत बड़े या जटिल होने पर अभिभूत हो जाते हैं, और काम पूरा करने से पहले ही मेमोरी या समय समाप्त होने के कारण रुक जाते हैं। बड़ा सवाल यह था: क्या इस तरह के कठिन मानचित्रों के लिए एक पूर्ण, प्रमाणित समाधान खोजने का कोई तरीका है बिना कंप्यूटर क्रैश हुए?

यह शोध पत्र "SAT सॉल्विंग" नामक एक उपकरण का उपयोग करके इस पहेली को हल करने का एक नया, अत्यंत स्मार्ट तरीका पेश करता है। एक SAT सॉल्वर को एक जासूस के रूप में सोचें जो यह जांचता है कि क्या नियमों का एक समूह एक ही समय में सत्य हो सकता है। लेखकों ने एक ऐसा ढांचा बनाया है जो केवल एक बार नियमों की जांच नहीं करता है; यह "हॉट एंड कोल्ड" का खेल खेलता है। यह अनुमत फ्रीक्वेंसी की एक विस्तृत श्रृंखला से शुरू होता है और जासूस से पूछता है, "क्या हम इतने में इसे कर सकते हैं?" यदि उत्तर "हाँ" है, तो जासूस एक समाधान ढूंढ लेता है, लेकिन ढांचा तुरंत कहता है, "ठीक है, लेकिन क्या हम इसे कम में कर सकते हैं?" यह नियमों को और कड़ा करता है और फिर से पूछता है। जादू का तरीका यह है कि जासूस पिछले "नहीं" उत्तरों से सीखी गई हर चीज़ को याद रखता है। हर बार शून्य से शुरुआत करने के बजाय, यह पिछले अनुभवों का उपयोग करके असंभव समाधानों के विशाल हिस्सों को छोड़ने के लिए करता है, जिससे खोज अविश्वसनीय रूप से तेज़ हो जाती है।

शोधकर्ताओं ने इस नए "इन्क्रीमेंटल SAT" दृष्टिकोण का परीक्षण 146 अलग-अलग प्रकार के मानचित्रों पर किया, जिनमें सरल रेखाएं और वृत्त से लेकर सांप और पेड़ों जैसी जटिल, घुमावदार संरचनाएं शामिल थीं। उन्होंने पाया कि उनका तरीका एक पावरहाउस था। इसने 38 बिल्कुल नए सर्वश्रेष्ठ-ज्ञात उत्तर खोज निकाले जो पहले किसी ने नहीं खोजे थे। इससे भी महत्वपूर्ण बात यह है कि उन्होंने सिद्ध किया कि इनमें से 109 समाधान वास्तव में सर्वश्रेष्ठ संभव समाधान थे, जो कि उन समाधानों की संख्या से बहुत अधिक है जिन्हें पिछले तरीकों द्वारा पुष्ट किया जा सका था। जबकि पुराने कंप्यूटर प्रोग्राम (ILP सॉल्वर) अभी भी सरल, "सपाट" मानचित्रों को हल करने के लिए सर्वश्रेष्ठ थे, नया SAT तरीका उन जटिल मानचित्रों में पूरी तरह से हावी रहा जहाँ बिंदुओं के बीच की दूरी बढ़ती जा रही थी। यह पता चला है कि SAT जासूस की स्मृति को पुराने प्रोग्रामों की शक्ति के साथ जोड़कर, टीम ने रेडियो फ्रीक्वेंसी पहेलियों को हल करने का एक तरीका खोल दिया है जिन्हें पहले पूरी तरह से हल करना बहुत कठिन माना जाता था।

तकनीकी सारांश: रेडियो $k$ -लेबलिंग के लिए एक SAT-आधारित सटीक दृष्टिकोण

समस्या की परिभाषा
यह शोध पत्र रेडियो $k$ -लेबलिंग समस्या (जिसे रेडियो $k$ -कलोरिंग भी कहा जाता है) को संबोधित करता है, जो कि चैनल असाइनमेंट समस्या से व्युत्पन्न एक कॉम्बिनेटरियल ऑप्टिमाइज़ेशन समस्या है। एक जुड़े हुए ग्राफ $G=(V, E)$ के लिए, जिसका व्यास (diameter) $k = \text{diam}(G)$ है, उद्देश्य शीर्षों (vertices) को गैर-ऋणात्मक पूर्णांक लेबल $f(v)$ प्रदान करना है ताकि प्रत्येक दो भिन्न शीर्षों $u, v$ के लिए, स्थिति $|f(u) - f(v)| \ge k + 1 - d(u, v)$ बनी रहे, जहाँ $d(u, v)$ लघुतम पथ दूरी (shortest path distance) है। लक्ष्य लेबलिंग के स्पैन (span) को कम करना है, जिसे $\max_{v \in V} f(v)$ के रूप में परिभाषित किया गया है। संभव न्यूनतम स्पैन को रेडियो संख्या (radio number), $rn(G)$ कहा जाता है।

जबकि विशिष्ट ग्राफ परिवारों (जैसे पाथ, साइकिल, ट्री) के लिए सैद्धांतिक निर्माण मौजूद हैं और सामान्य ग्राफों के लिए ह्यूरिस्टिक एल्गोरिदम व्यवहार्य समाधान प्रदान करते हैं, व्यापक ग्राफ वर्गों के लिए सटीक समाधान दुर्लभ हैं। मौजूदा इंटीजर लीनियर प्रोग्रामिंग (ILP) फॉर्मूलेशन स्केलेबिलिटी संबंधी समस्याओं से ग्रस्त हैं, जिसका कारण खोज स्थान (search space) का तेजी से बढ़ना और अनुकूलन पुनरावृत्तियों (optimization iterations) के बीच सूचना का पुन: उपयोग न हो पाना है।

कार्यप्रणाली (Methodology)
लेखक एक सटीक, इंक्रीमेंटल SAT-आधारित फ्रेमवर्क प्रस्तावित करते हैं जो एक कॉम्पैक्ट ऑर्डर एनकोडिंग को एक पुनरावृत्ति अनुकूलन रणनीति के साथ जोड़ता है।

SAT एनकोडिंग्स:
शोध पत्र लेबल डोमेन $\{1, \dots, UB\}$ पर आधारित दो बूलियन सैटिस्फिएबिलिटी (SAT) एनकोडिंग्स विकसित करता है, जहाँ $UB$ एक पूर्व-निर्धारित ऊपरी सीमा (upper bound) है:

डायरेक्ट एनकोडिंग (Direct Encoding): यह असाइनमेंट वेरिएबल्स $x_{v,l}$ (सत्य यदि शीर्ष $v$ का लेबल $l$ है) का उपयोग करता है। यह युग्मवार संघर्ष क्लॉज़ (pairwise conflict clauses) के माध्यम से बाधाओं को लागू करता है। यद्यपि यह तार्किक रूप से ILP मॉडल के समान है, इसके लिए रेडियो बाधाओं हेतु $O(n^2 UB k)$ क्लॉज़ की आवश्यकता होती है, जिससे यूनिट रेजोल्यूशन के तहत कमजोर प्रोपेगेशन होता है।
ऑर्डर एनकोडिंग (Order Encoding): यह असाइनमेंट वेरिएबल्स के साथ थ्रेशोल्ड वेरिएबल्स $g_{v,l}$ (सत्य यदि $f(v) \ge l$ ) पेश करता है। यह एनकोडिंग रेडियो बाधा $|f(u) - f(v)| \ge \Delta_{uv}$ को अधिक कॉम्पैक्ट तरीके से प्रस्तुत करती है। यह क्लॉज़ काउंट में $k$ पर निर्भरता को समाप्त करके रेडियो बाधा क्लॉज़ की संख्या को $O(n^2 UB k)$ से घटाकर $O(n^2 UB)$ कर देता है। ऑर्डर एनकोडिंग मजबूत प्रोपेगेशन को भी सक्षम बनाती है, क्योंकि असमानताएं जैसे $f(v) \ge c$ एकल लिटरल (literal) में मैप होती हैं।

इंक्रीमेंटल सॉल्विंग रणनीति:
फ्रेमवर्क एक इंक्रीमेंटल SAT सॉल्विंग प्रतिमान (paradigm) का उपयोग करता है। प्रत्येक पुनरावृत्ति के लिए फॉर्मूला को फिर से बनाने के बजाय, एक ही सॉल्वर इंस्टेंस बनाया जाता है। एल्गोरिदम इस प्रकार कार्य करता है:

चरण 1: सभी-जोड़ियों की दूरियाँ (all-pairs distances) की गणना करें और $k = \text{diam}(G)$ सेट करें।
चरण 2: प्रारंभिक ऊपरी सीमा $UB$ के साथ SAT मॉडल बनाएँ।
चरण 3: फॉर्मूला को पुनरावृत्ति (iteratively) के रूप में हल करें। यदि स्पैन $\beta$ के साथ एक संतोषजनक असाइनमेंट मिलता है, तो सॉल्वर को किसी भी स्पैन $\ge \beta$ को वर्जित करने (सीमा को कड़ा करने) के निर्देश दिए जाते हैं और पुनः हल किया जाता है। महत्वपूर्ण रूप से, पिछले पुनरावृत्तियों से सीखे गए क्लॉज़ (learned clauses) सुरक्षित रखे जाते हैं, जिससे रेडंडेंट सर्च प्रयास से बचा जा सके। लूप तब समाप्त होता है जब सॉल्वर UNSAT लौटाता है (अनुकूलता प्रमाणित करता है) या समय सीमा समाप्त हो जाती है।

सिमेट्री ब्रेकिंग (Symmetry Breaking):
साइकिल ग्राफ ( $C_n$ ) के लिए, जो रोटेशनल सिमेट्री प्रदर्शित करते हैं, लेखक एक सिमेट्री-ब्रेकिंग बाधा पेश करते हैं जो पहले शीर्ष के लेबल को 1 ( $f(0)=1$ ) पर स्थिर करती है। यह खोज स्थान को कम करता है और अनुकूल समाधानों को छोड़े बिना अनुकूलता के प्रमाण को महत्वपूर्ण रूप से तेज करता है।

प्रमुख योगदान

नवीन फ्रेमवर्क: ऑर्डर एनकोडिंग और इंक्रीमेंटल सॉल्विंग का उपयोग करते हुए रेडियो $k$ -लेबलिंग समस्या के लिए पहला सामान्य सटीक SAT-आधारित अनुकूलन फ्रेमवर्क।
दक्षता में सुधार: ऑर्डर एनकोडिंग डायरेक्ट एनकोडिंग की तुलना में क्लॉज़ जटिलता को कम करती है और प्रोपेगेशन में सुधार करती है। इंक्रीमेंटल दृष्टिकोण सीखे गए क्लॉज़ का पुन: उपयोग करता है, जो स्वतंत्र SAT कॉल्स या मानक ILP दृष्टिकोणों की तुलना में, जो पिछले खोज डेटा को हटा देते हैं, कंप्यूटेशनल ओवरहेड को काफी कम करता है।
सिमेट्री हैंडलिंग: साइकिल ग्राफों के लिए विशिष्ट सिमेट्री-ब्रेकिंग बाधाओं का परिचय, जो समाधान समय में पर्याप्त तेजी और प्रमाणित अनुकूल परिणामों की संख्या में वृद्धि प्रदर्शित करता है।

प्रायोगिक परिणाम
फ्रेवर्क का मूल्यांकन नौ ग्राफ परिवारों (पाथ, साइकिल, ट्राइएंगुलर स्नेक्स, $kC_m$ -स्नेक्स, लैडर्स, बुक्स, फ्रेंडशिप ग्राफ्स और बाइनोमियल ट्रीज़) के 146 बेंचमार्क इंस्टेंस पर 1,200 सेकंड की समय सीमा के साथ किया गया।

ह्यूरिस्टिक्स के विरुद्ध प्रदर्शन: प्रस्तावित Order-SAT विधि ने उन 98 इंस्टेंसों में से 38 नए सर्वश्रेष्ठ-ज्ञात रेडियो नंबर स्थापित किए जिनका कोई ज्ञात क्लोज्ड-फॉर्म ऑप्टिममम नहीं था। इसने मौजूदा ह्यूरिस्टिक्स (Ub1, Ub3) और डायरेक्ट-एनकोडिंग SAT की तुलना में लगातार अधिक सटीक व्यवहार्य सीमाएँ (feasible bounds) प्रदान कीं।
ILP के विरुद्ध प्रदर्शन:
- बढ़ते-व्यास वाले ग्राफ (Growing-Diameter Graphs): उन परिवारों के लिए जहाँ व्यास आकार के साथ बढ़ता है (जैसे स्नेक्स, लैडर्स, बाइनोमियल ट्रीज़), Order-SAT ने समाधान की गुणवत्ता (तटस्थ सीमाएँ) और प्रमाणित अनुकूल परिणामों की संख्या दोनों में वाणिज्यिक ILP सॉल्वर (CPLEX, Gurobi) को पछाड़ दिया। ILP सॉल्वर अक्सर इन इंस्टेंसों पर मेमोरी समाप्त कर देते थे या ढीले इन्कंबेंट्स (loose incumbents) लौटाते थे।
- सीमित-व्यास वाले ग्राफ (Bounded-Diameter Graphs): उन परिवारों के लिए जिनका व्यास स्थिर है (जैसे बुक ग्राफ्स, फ्रेंडशिप ग्राफ्स), ILP सॉल्वर अधिक प्रभावी थे, जिन्होंने सभी इंस्टेंसों के लिए अनुकूलता को जल्दी प्रमाणित किया।
संयुक्त दृष्टिकोण: SAT फ्रेमवर्क को ILP मॉडल के साथ जोड़कर, इस अध्ययन ने 146 में से 109 इंस्टेंस के लिए अनुकूल समाधान प्रमाणित किए, जिससे प्रमाणित अनुकूलता के साथ रेडियो-लेबलिंग बेंचमार्क का विस्तार हुआ।
सांख्यिकीय महत्व: फ्रीडमैन टेस्ट (Friedman test) ने पुष्टि की कि Order-SAT ने सभी तुलना किए गए तरीकों, जिनमें वाणिज्यिक सॉल्वर और ह्यूरिस्टिक्स शामिल हैं, में सर्वश्रेष्ठ समग्र रैंकिंग (औसत रैंक 2.58) प्राप्त की।

महत्व
यह शोध पत्र दावा करता है कि इंक्रीमेंटल SAT सॉल्विंग ग्राफ लेबलिंग समस्याओं के लिए एक व्यावहारिक सटीक अनुकूलन प्रतिमान (practical exact optimization paradigm) है, जो पारंपरिक रूप से सैद्धांतिक निर्माणों और ह्यूरिस्टिक एल्गोरिदम द्वारा हावी रही हैं। यह कार्य दर्शाता है कि:

आधुनिक SAT सॉल्वर, कॉम्पैक्ट एनकोडिंग और इंक्रीमेंटल रणनीतियों के साथ मिलकर, उन कठिन कॉम्बिनेटरियल ऑप्टिमाइज़ेशन समस्याओं को हल कर सकते हैं जहाँ पारंपरिक ILP फॉर्मूलेशन स्केलेबिलिटी के कारण संघर्ष करते हैं।
प्रस्तावित दृष्टिकोण ILP के पूरक है; यह बढ़ते व्यास वाले ग्राफों के लिए श्रेष्ठ है, जबकि सीमित व्यास वाले ग्राफों के लिए ILP अधिक उपयुक्त रहता है।
फ्रेमवर्क सफलतापूर्वक सैद्धांतिक सीमाओं और प्रमाणित सटीक समाधानों के बीच के अंतर को पाटता है, जो जटिल ग्राफ संरचनाओं में रेडियो नंबर निर्धारित करने के लिए एक मजबूत उपकरण प्रदान करता है।

लेखक निष्कर्ष निकालते हैं कि यह दृष्टिकोण विशिष्ट ग्राफ वर्गों के लिए वाणिज्यिक सॉल्वरों के लिए एक अत्यधिक प्रतिस्पर्धी विकल्प प्रदान करता है और अन्य ग्राफ लेबलिंग और कॉम्बिनेटरियल ऑप्टिमाइज़ेशन समस्याओं के लिए इंक्रीमेंटल SAT सॉल्विंग की क्षमता को उजागर करता है।

इसी तरह के और पेपर