North-East Lattice Paths Avoiding $k$ Collinear Points via Satisfiability

तकनीकी सारांश: संतुष्टि (Satisfiability) के माध्यम से $k$ संरेखीय बिंदुओं (Collinear Points) से बचने वाले उत्तर-पूर्व जाली पथ (North–East Lattice Paths)

समस्या की परिभाषा
यह शोध पत्र जेरवर-रैम्से (Gerver–Ramsey) संरेखीयता समस्या की जांच करता है, जो एक उत्तर-पूर्व जाली पथ (कदम: $\{(1,0), (0,1)\}$) की अधिकतम लंबाई निर्धारित करने का प्रयास करती है जो $k$ संरेखीय बिंदुओं को समाहित करने से बचता है। मान लीजिए कि $a(k)$ वह लघुतम पूर्णांक है कि प्रत्येक उत्तर-पूर्व जाली पथ जिसकी लंबाई $a(k)$ है, उसमें $k$ संरेखीय बिंदु अवश्य होंगे; फलस्वरूप, $a(k)-1$ ऐसे लंबे पथ की लंबाई है जो $k$ संरेखीय बिंदुओं से बचता है। जबकि मोंटगोमरी (1972) ने सिद्ध किया कि सभी $k$ के लिए ऐसा एक ऊपरी स्तर (bound) मौजूद है, और जेरवर एवं रैम्से (1979) ने एक स्पष्ट लेकिन अत्यंत ढीला ऊपरी स्तर प्रदान किया, छोटे $k$ के लिए $a(k)$ के सटीक मान काफी हद तक अज्ञात या सत्यापन के लिए कठिन बने हुए थे। इस कार्य से पूर्व, जे. शालिट (Shallit, 2013) ने गणनात्मक रूप से $a(4)=9$, $a(5)=29$, और $a(6)=97$ निर्धारित किया था, और एक 261 लंबाई के पथ को खोजकर $a(7) \ge 261$ का निचला स्तर (lower bound) स्थापित किया था।

कार्यप्रणाली (Methodology)
लेखक इन जाली पथों को खोजने और सत्यापित करने के लिए बूलियन संतुष्टि (Boolean Satisfiability - SAT) समाधान का उपयोग करते हैं। मुख्य दृष्टिकोण $k$ संरेखीय बिंदुओं से बचने वाले लंबाई $m$ के पथ के अस्तित्व को एक कंजंक्टिव नॉर्मल फॉर्म (CNF) सूत्र के रूप में कूटबद्ध (encode) करना है।

1. SAT एन्कोडिंग:

   • चर (Variables): बूलियन चर $v_{x,y}$ यह दर्शाते हैं कि बिंदु $(x,y)$ पथ पर है या नहीं।
   • पथ प्रतिबंध (Path Constraints): क्लॉज (clauses) यह सुनिश्चित करते हैं कि पथ $(0,0)$ से शुरू होता है, केवल उत्तर या पूर्व की ओर बढ़ता है, और विभाजित नहीं होता है (अर्थात, किसी भी बिंदु से, पथ अगले दो संभावित बिंदुओं में से ठीक एक की ओर बढ़ता है)।
   • गैर-संरेखता प्रतिबंध (Non-Collinearity Constraints): लेखक कार्डिनैलिटी बाधाओं (at-most-$k$) का उपयोग करते हैं ताकि यह सुनिश्चित हो सके कि कोई भी रेखा $k$ बिंदुओं को नहीं समाहित करती है। इन्हें अनुक्रमिक काउंटर एन्कोडिंग का उपयोग करके CNF में कूटबद्ध किया गया है या 'klauses' का उपयोग करके "at-least-$k$ conjunctive normal form" (KNF) के माध्यम से संभाला गया है।
   • अनुकूलन (Optimizations):
     • सममिति भंग (Symmetry Breaking): पूरक समरूपता (complementation symmetry) को समाप्त करने के लिए पहले कदम को उत्तर की ओर होने का नियम लागू करके खोज स्थान को कम किया गया है। आइसोमॉर्फिज्म (isomorphism) जाँच के लिए रिवर्सल सिमेट्री को खोज के दौरान काफी हद तक अनदेखा किया गया था।
     • पहुंच क्षमता सीमाएँ (Reachability Bounds): उन बिंदुओं को जो अप्राप्य सिद्ध हुए हैं (जैसे, जिन्हें एक ही दिशा में $k-1$ लगातार कदमों की आवश्यकता है), उन्हें यूनिट क्लॉज के माध्यम से अवरुद्ध किया गया है।
     • प्रतिबंध हटाने का ह्यूरिस्टिक (Constraint Removal Heuristic): दक्षता सुधारने के लिए, संबंधित क्षेत्र में बहुत कम बिंदुओं वाली रेखाओं के गैर-संरेखता प्रतिबंधों को हटा दिया जाता है। यदि कोई समाधान मिलता है, तो यह सुनिश्चित करने के लिए कि कोई $k$ संरेखीय बिंदु मौजूद नहीं हैं, उसे स्पष्ट रूप से सत्यापित किया जाता है।
     • समानांतरकरण (Parallelization): बड़े उदाहरणों के लिए, "क्यूब-एंड-कंकर" (cube-and-conquer) तकनीक का उपयोग किया जाता है। एक लुकअहेड सॉल्वर (march) खोज स्थान को विसंयुक्त उप-समस्याओं (cubes) में विभाजित करता है, जिन्हें फिर समानांतर में हल किया जाता है।

2. सॉल्वर चयन:

   • लेखकों ने मानक CNF एन्कोडिंग (जिसे CaDiCaL द्वारा हल किया गया) की तुलना KNF एन्कोडिंग (जिसे Cardinality-CaDiCaL द्वारा हल किया गया) से बेंचमार्क की।
   • परिणामों से संकेत मिला कि संतोषजनक (satisfiable) मामलों में (लंबे पथ खोजने के लिए) KNF काफी बेहतर प्रदर्शन करता है, जबकि असंतोषजनक (unsatisfiable) मामलों में (लंबे पथों के गैर-अस्तित्व को सिद्ध करने के लिए) CNF श्रेष्ठ है। कार्यप्रणाली लक्ष्य (पथ खोजना या गैर-अस्तित्व सिद्ध करना) के आधार पर एन्कोडिंग प्रकार को अनुकूलित करती है।

मुख्य परिणाम
शोध पत्र निम्नलिखित गणनात्मक परिणाम प्रस्तुत करता है:

• $k \le 6$ के लिए गणना (Enumeration): लेखकों ने $k \le 6$ के लिए आइसोमॉर्फिज्म तक सभी maximal GR($k$) वॉक (लंबाई $a(k)-1$ वाले पथ) को व्यापक रूप से सूचीबद्ध किया।

  • पिछले परिणामों की पुष्टि की: $a(4)=9$, $a(5)=29$, और $a(6)=97$।
  • पाया कि दो अलग-अलग maximal GR(4) वॉक, एक अद्वितीय maximal GR(5) वॉक, और दो अलग-अलग maximal GR(6) वॉक मौजूद हैं।
  • लंबी पथों के गैर-अस्तित्व के लिए DRAT प्रमाण प्रमाणपत्र (proof certificates) उत्पन्न किए, जिससे SAT सॉल्वर पर भरोसा किए बिना स्वतंत्र सत्यापन संभव हुआ।

• $k = 7$ के लिए प्रगति:

  • निचले स्तर (Lower Bound) में सुधार: लेखकों ने 327 चरणों वाला एक GR(7) वॉक खोजा, जो शालिट द्वारा खोजे गए पिछले सर्वोत्तम ज्ञात 260 चरणों की लंबाई में उल्लेखनीय सुधार है।
  • पहुंच क्षमता विश्लेषण (Reachability Analysis): उन्होंने 267 चरणों तक GR(7) वॉक के ऊपरी और निचले पहुंच क्षमता स्तरों को निर्धारित किया और रेखा $y=x+1$ पर पहला अप्राप्य बिंदु $(146, 147)$ की पहचान की।
  • खोज रणनीति: सबसे लंबे वॉक को रैंडम सीड समानांतरकरण और क्यूब-एंड-कंकर के हाइब्रिड दृष्टिकोण का उपयोग करके खोजा गया। विशेष रूप से, खोजे गए सबसे लंबे वॉक रेखा $y=x+1$ के निकट केंद्रित थे।

महत्व और दावे
यह शोध पत्र दावा करता है कि SAT सॉल्वर न केवल विशाल खोज स्थानों वाले असतत ज्यामिति (discrete geometry) की समस्याओं को हल करने के लिए प्रभावी हैं, बल्कि वे प्रमाण प्रमाणपत्र (DRAT प्रारूप) उत्पन्न करने की क्षमता के कारण कस्टम-लिखित खोज कोड की तुलना में उच्च स्तर का विश्वास भी प्रदान कर सकते हैं।

प्रमुख योगदान हैं:

1. लंबे GR($k$) वॉक खोजने और उनकी व्यापकता सिद्ध करने के लिए एक SAT-आधारित विधि।
2. $k \le 6$ के लिए पूर्ण maximal GR($k$) वॉक का विवरण, जो पिछले गणनात्मक परिणामों की पुष्टि और विस्तार करता है।
3. $a(7)$ के लिए एक नया निचला स्तर, जो ज्ञात सबसे लंबे पथ को 260 से बढ़ाकर 327 चरणों तक ले जाता है।
4. एक प्रयोगात्मक अध्ययन जो प्रदर्शित करता है कि यद्यपि $a(7)$ का सटीक मान अभी भी अज्ञात है, SAT समाधान प्रभावी रूप से खोज स्थान में नेविगेट कर सकता है और प्रमाण प्रमाणपत्र भी उत्पन्न किए जा सकते हैं।

लेखक $a(7)$ के निर्धारण के संबंध में विनम्र बने हुए हैं, यह नोट करते हुए कि सटीक मान अभी भी अज्ञात है, लेकिन उन्हें उम्मीद है कि इस समस्या में SAT समाधान का उनका परिचय आगे की प्रगति को सुगम बनाएगा।