On Proof Systems for #QBF

शीर्षक: #QBF के लिए प्रमाण प्रणालियों पर

समस्या विवरण
यह शोध पत्र #QBF समस्या को संबोधित करता है, जिसमें एक क्वांटिफाइड बुलियन फॉर्मूला (QBF) के लिए अस्तित्वपरक खिलाड़ी (existential player) की जीतने वाली रणनीतियों की संख्या ज्ञात करना शामिल है। इस समस्या को #PSPACE-पूर्ण के रूप में पहचाना गया है, जो इसे एनालॉगस #SAT समस्या (प्रपोजिशनल फॉर्मूला के लिए मॉडल काउंटिंग) की तुलना में गणनात्मक रूप से अधिक कठिन बनाता है, जहाँ समाधानों की संख्या अधिकतम घातांकीय (exponential) होती है। इसके विपरीत, #QBF में जीतने वाली रणनीतियों की संख्या दोहरी घातांकीय (doubly exponential) हो सकती है। जबकि QBF के लिए प्रमाण प्रणालियों (जैसे Q-Res, ∀Exp) और #SAT के लिए प्रमाण प्रणालियों (जैसे KCPS, CPOG, CLIP, MICE) का अध्ययन किया गया है, सामान्य #QBF समस्या के लिए समर्पित प्रमाण प्रणालियों का अभाव था जो जीतने वाली रणनीतियों की गणना को प्रमाणित कर सकें। मौजूदा सॉल्वर जैसे d4-QBF और qCounter मौजूद हैं लेकिन प्रमाणन के लिए एक औपचारिक प्रमाण जटिलता ढांचे (formalized proof complexity framework) की कमी है।

कार्यप्रणाली
लेखक QBF प्रमाण प्रणालियों और #SAT प्रमाण प्रणालियों दोनों की अवधारणाओं का विस्तार करते हुए #QBF के लिए नई प्रमाण प्रणालियाँ डिजाइन करते हैं। वे तीन अलग-अलग दृष्टिकोणों का अन्वेषण करते हैं:

1. नाइटीव सिस्टम (Naive System): एक प्रारंभिक प्रणाली जो सभी $k$ जीतने वाली रणनीतियों को सूचीबद्ध करती है। यह प्रत्येक रणनीति की शुद्धता को प्रमाणित करके (Skolem functions के tautology प्रमाणों के माध्यम से), रणनीतियों की विशिष्टता को प्रमाणित करके (witness assignments के माध्यम से), और किसी अन्य रणनीति के अस्तित्व को प्रमाणित न करके (एक false QBF एन्कोडिंग के माध्यम से) गणना को प्रमाणित करती है। लेखक नोट करते हैं कि यह प्रणाली तब मामूली निचली सीमाओं (trivial lower bounds) से ग्रस्त होती है जब रणनीतियों की संख्या दोहरी घातांकीय होती है।
2. विस्तार-आधारित प्रणाली (Expansion-based System - ∀Exp+MICE): यह दृष्टिकोण QBF सॉल्विंग में उपयोग किए जाने वाले ∀-expansion नियम को अनुकूलित करता है। यह यूनिवर्सल वेरिएबल्स के सभी संभावित असाइनमेंट पर QBF को सिमेंटिक रूप से विस्तारित करता है, जिससे #QBF समस्या को #SAT समस्या में बदल दिया जाता है। परिणामी CNF को फिर #SAT प्रमाण प्रणाली MICE द्वारा प्रोसेस किया जाता है। लेखक तर्क देते हैं कि यह प्रणाली स्वाभाविक रूप से यूनिवर्सल वेरिएबल्स के सापेक्ष घातांकीय आकार की आवश्यकता रखती है क्योंकि इसे मॉडल काउंट को बनाए रखने के लिए सभी यूनिवर्सल असाइनमेंट को विस्तारित करना पड़ता है।
3. लाइन-आधारित प्रणाली (Line-based System - Q-MICE): मुख्य योगदान Q-MICE (क्वांटिफाइड मॉडल-काउंटिंग इंडक्शन बाय क्लेम एक्सटेंशन) का प्रस्ताव है। #SAT के लिए MICE प्रणाली से प्रेरित, Q-MICE एक लाइन-आधारित प्रमाण प्रणाली है जहाँ प्रत्येक लाइन $(Q.F, A, c)$ के रूप में एक दावा है।
   • $Q.F$: एक सत्य QBF।
   • $A$: अस्तित्वपरक वेरिएबल्स के एक उपसमुच्चय के लिए Skolem functions के साथ एक आंशिक रणनीति।
   • $c$: उन तरीकों की संख्या जिनसे $A$ को पूर्ण जीतने वाली रणनीतियों में विस्तारित किया जा सकता है।
   • अनुमान नियम (Inference Rules): Q-MICE तीन मुख्य नियमों का उपयोग करता है:
     • एक्सिओम नियम (Axiom Rule): उन प्रतिबंधित QBFs के लिए दावों को व्युत्पन्न करता है जहाँ मैट्रिक्स एक tautology है, जिससे एक्सटेंशन की प्रत्यक्ष कॉम्बिनेटरियल काउंटिंग संभव होती है।
     • कंपोजिशन नियम (Composition Rules): दावों को संयोजित करने या सरल बनाने की अनुमति देते हैं। Composition-a विशिष्ट पूर्ण रणनीतियों को जोड़ता है; Composition-b रणनीति प्रतिबंधों को तब हटा देता है जब विशिष्टता सिद्ध हो जाती है; Composition-c उन दावों को जोड़ता है जहाँ रणनीतियाँ विशिष्ट वेरिएबल्स पर भिन्न होती हैं, बशर्ते कि "मॉडल की अनुपस्थिति" का प्रमाण यह प्रमाणित करे कि कोई अन्य रणनीतियाँ मौजूद नहीं हैं।
     • जॉइन नियम (Join Rule): दो दावों को जोड़ता है जो केवल एक यूनिवर्सल वेरिएबल पर प्रतिबंध द्वारा भिन्न होते हैं, उनके काउंट को गुणा करता है, बशर्ते कि असाइनमेंट ट्री की संरचना (path graphs) इसकी अनुमति दे।

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

• Q-MICE का औपचारिकीकरण: लेख में Q-MICE को परिभाषित किया गया है और सिद्ध किया गया है कि यह सुसंगत और पूर्ण है (प्रमेय 16)। यह बहुपद-समय (polynomial-time) सत्यापन योग्य है।
• घातांकीय पृथक्करण (Exponential Separation): लेखक प्रदर्शित करते हैं कि Q-MICE, नाइटीव सिस्टम और ∀Exp+MICE दोनों की तुलना में घातांकीय रूप से अधिक शक्तिशाली है (प्रमेय 17)।
  • XOR-PAIRS परिवार: वे प्रपोजिशनल XOR-PAIRS फॉर्मूला का एक क्वांटिफाइड संस्करण पेश करते हैं। जबकि यह परिवार ∀Exp+MICE में सुपर-पॉलिनोमियल (घातांकीय) प्रमाणों की आवश्यकता रखता है क्योंकि इसे यूनिवर्सल वेरिएबल्स को विस्तारित करने की आवश्यकता होती है, Q-MICE Axiom और Composition-b नियमों का उपयोग करके एक स्थिर-लंबाई वाला, बहुपद-आकार का प्रमाण प्रदान करता है।
  • इंडेक्स्ड एफ़ाइन QBF परिवार: वे एक सरल एन्क्रिप्शन प्रक्रिया का प्रतिनिधित्व करने वाले QBFs के एक परिवार का निर्माण करते हैं। इस परिवार में $2^n$ जीतने वाली रणनीतियाँ हैं, जो नाइटीव और ∀Exp+MICE दोनों प्रणालियों में घातांकीय प्रमाणों की आवश्यकता पैदा करती हैं। Q-MICE कंपोजिशन और जॉइन नियमों को पुनरावृत्त रूप से लागू करके एक रैखिक-लंबाई वाला, बहुपद-आकार का प्रमाण संभालता है।
• संरचनात्मक विश्लेषण: लेख रेखांकित करता है कि विस्तार-आधारित प्रणालियाँ यूनिवर्सल वेरिएबल्स के साथ निपटने में अंतर्निहित संरचनात्मक कमजोरियों (घातांकीय विस्फोट) से ग्रस्त होती हैं, जबकि Q-MICE दक्षता बनाए रखने के लिए क्वांटिफायर हैंडलिंग को काउंटिंग के साथ इंटरलीव करता है।

महत्व और दावे
लेख का दावा है कि Q-MICE जैसी प्रमाण प्रणालियों का अस्तित्व #QBF के सिद्धांत को आगे बढ़ाने और #QBF सॉल्वर की शुद्धता को प्रमाणित करने के लिए महत्वपूर्ण है, जो कि वर्तमान में अपने प्रारंभिक चरणों में है। बिना सभी रणनीतियों को सूचीबद्ध किए मॉडल काउंट को प्रमाणित करने का ढांचा प्रदान करके, Q-MICE अधिक मजबूत सॉल्वर सत्यापन की ओर एक मार्ग प्रदान करता है।

लेखक विनम्रतापूर्वक नोट करते हैं कि यद्यपि Q-MICE शक्तिशाली है, लेकिन इसमें अभी तक d4-QBF जैसे अत्याधुनिक सॉल्वरों में पाए जाने वाले डिकंपोजिशन नियम शामिल नहीं हैं, हालांकि वे सुझाव देते हैं कि इसे एक मॉड्यूलर अनुमान नियम के रूप में जोड़ा जा सकता है। वे खुले प्रश्नों की भी पहचान करते हैं, जिनमें Q-MICE के लिए वास्तविक निचली सीमाएं स्थापित करना (यह अनुमान लगाते हुए कि प्रपोजिशनल XOR-PAIRS इसके लिए कठिन हो सकता है, हालांकि यह अभी तक एक सिद्ध निचली सीमा नहीं है) और अन्य #SAT प्रमाण प्रणालियों (CPOG, CLIP, KCPS) को #QBF डोमेन में विस्तारित करना शामिल है। यह शोध पत्र कोई नया प्रयोगात्मक सॉल्वर प्रस्तावित नहीं करता है बल्कि पूरी तरह से सैद्धांतिक प्रमाण जटिलता और इन प्रणालियों के पृथक्करण पर ध्यान केंद्रित करता है।