💻 computer science

d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries

यह शोध पत्र एक सामान्य ढांचे को प्रस्तुत करता है जो इनपुट सूत्रों को पूर्व-गणना किए गए सिद्धांत लेम्मा (theory lemmas) के साथ जोड़कर नॉलेज कंपाइलेशन को सैटिस्फिएबिलिटी मॉड्यूल थ्योरीज (SMT) तक विस्तारित करता है ताकि संकलित SMT d-DNNFs की पॉलीटाइम प्रपोजीशनल-शैली की क्वेरी करने में सक्षम बनाया जा सके।

मूल लेखक: Gabriele Masina, Emanuale Civini, Massimo Michelutti, Giuseppe Spallitta, Roberto Sebastiani

प्रकाशित 2026-03-11

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

CC BY 4.0

मूल लेखक: Gabriele Masina, Emanuale Civini, Massimo Michelutti, Giuseppe Spallitta, Roberto Sebastiani

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

यहाँ "d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries" का सरल भाषा और रचनात्मक उपमाओं (analogies) का उपयोग करके किया गया स्पष्टीकरण है।

बड़ी तस्वीर: "पहले से पका हुआ भोजन" (Pre-Cooked Meal) की रणनीति

कल्पना कीजिए कि आप एक उच्च श्रेणी का रेस्टोरेंट चलाते हैं। आपके ग्राहक (कंप्यूटर प्रोग्राम) आपसे आपके मेनू के बारे में जटिल प्रश्न पूछते रहते हैं, जैसे "क्या कोई ऐसा व्यंजन है जो तीखा भी हो और शाकाहारी भी?" या "20 डॉलर के तहत भोजन ऑर्डर करने के कितने अलग-अलग तरीके हैं?"

पुराना तरीका (Standard SMT Solvers):
हर बार जब कोई ग्राहक सवाल पूछता है, तो आप रसोई में भागते हैं, कच्चा माल निकालते हैं, उसे काटते हैं, पकाते हैं, चखते हैं, और फिर सवाल का जवाब देते हैं। यदि सवाल कठिन है, तो रसोई में अफरा-तफरी मच जाती है और इसमें बहुत समय लगता है। यदि 1,000 ग्राहक सवाल पूछते हैं, तो आप 1,000 अलग-अलग कुकिंग मैराथन करते हैं।

नया तरीका (इस पेपर का दृष्टिकोण):
यह पेपर एक अलग रणनीति प्रस्तावित करता है: नॉलेज कंपाइलेशन (Knowledge Compilation)।
ऑन-डिमांड खाना पकाने के बजाय, आप रेस्टोरेंट खोलने से पहले (ऑफलाइन चरण में) एक विशाल, पूरी तरह से व्यवस्थित मास्टर रेसिपी बुक (d-DNNF) तैयार करने में बहुत अधिक समय बिताते हैं।

एक बार जब यह किताब लिख ली जाती है, तो किसी भी सवाल का जवाब देना तुरंत हो जाता है। आप बस एक पन्ना पलटते हैं, इंडेक्स देखते हैं, और एक सेकंड के भीतर "हाँ" या "नहीं" कह देते हैं। कठिन काम पहले ही किया जा चुका था, इसलिए दैनिक कार्य आसान है।

समस्या: "विदेशी भाषा" की बाधा

यहाँ एक पेच है। "मास्टर रेसिपी बुक" (d-DNNF) एक बहुत ही सरल भाषा में लिखी गई है: प्रोपोजिशनल लॉजिक (सत्य/असत्य स्विच, जैसे लाइट बल्ब)।

लेकिन वास्तविक दुनिया (SMT - Satisfiability Modulo Theories) अधिक जटिल है। इसमें गणित (जैसे "x + y = 5"), एरेज़ (Arrays), या बिट-वेक्टर्स शामिल हैं।

प्रोपोजिशनल लॉजिक: "क्या लाइट चालू है?"
SMT: "क्या तापमान 20 और 30 डिग्री के बीच है?"

यदि आप गणित को बिना सोचे-समझे लाइट स्विच में अनुवाद करते हैं, तो आप एक ऐसी रेसिपी बुक बनाएंगे जो टूटी हुई होगी। यह कह सकती है "हाँ, आप एक ही समय में गर्म सूप और ठंडा आइसक्रीम ले सकते हैं" (जो भौतिकी के नियमों के अनुसार गणितीय रूप से असंभव है, लेकिन यदि आपको भौतिकी के नियम नहीं पता तो तार्किक रूप से संभव है)।

चुनौती: हम एक ऐसी "लाइट स्विच" रेसिपी बुक कैसे बनाएं जो "भौतिकी" (गणित/थ्योरी) के नियमों का सम्मान करती हो ताकि उत्तर हमेशा सही हों?

समाधान: "रूलबुक" एड-ऑन

लेखकों का जीनियस विचार यह है कि भौतिकी के नियमों को पहले से ही कंप्यूट (pre-compute) करें और रेसिपी बुक बनाने से पहले उन्हें इसमें जोड़ दें।

"आलसी" दृष्टिकोण (पुराना तरीका): जब कोई ग्राहक सवाल पूछता है, तो शेफ भौतिकी के नियमों की जाँच करता है। यदि नियमों का उल्लंघन होता है, तो वे पीछे हटते हैं (backtrack) और फिर से कोशिश करते हैं। यह प्री-कुक्ड बुक के लिए धीमा है क्योंकि बुक को किसी के पूछने से पहले ही परफेक्ट होना चाहिए।
"तत्पर" दृष्टिकोण (यह पेपर): रेसिपी बुक बनाने से पहले ही, हम एक बहुत बुद्धिमान सहायक (Theory Lemma Enumerator) से पूछते हैं कि वे हर उस नियम की सूची बना दे जो हमारे लॉजिक को तोड़ सकता है।
- उदाहरण: "आप एक ही समय में x > 5 और x < 3 नहीं रख सकते।"
- हम इन नियमों की सूची लेते हैं और खाना पकाने से पहले ही इन्हें सामग्री (ingredients) में जोड़ देते हैं।

अब, जब हम "लाइट स्विच" बुक बनाते हैं, तो हमें इन नियमों का पालन करने के लिए मजबूर किया जाता है। परिणामी बुक T-Reduced (थ्योरी-रिड्यूस्ड) होती है। इसमें कोई भी "असंभव" परिदृश्य नहीं होता।

यह व्यवहार में कैसे काम करता है

पेपर एक दो-चरणीय प्रक्रिया का वर्णन करता है:

चरण 1: "प्री-फ्लाइट" चेक (Compilation)

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

चरण 2: "तत्काल" उत्तर (Querying)

इनपुट: एक प्रश्न (जैसे, "क्या यह परिदृश्य संभव है?")।
क्रिया: आप एक मानक, तेज़ टूल का उपयोग करते हैं जो सरल True/False लॉजिक के लिए बनाया गया है (प्रोपोजिशनल रीज़नर)।
परिणाम: चूंकि "असंभव" गणितीय परिदृश्यों को चरण 1 के दौरान ही हटा दिया गया था, इसलिए सरल टूल आपको तुरंत सही उत्तर देता है।
उपमा: एक ग्राहक पूछता है, "क्या मैं एक तीखा शाकाहारी व्यंजन ले सकता हूँ?" आप अपनी रंग-कोडित पेंट्री को देखते हैं। चूंकि आपने तैयारी के दौरान ही सभी गैर-शाकाहारी और गैर-तीखी वस्तुओं को हटा दिया था, इसलिए आप बस लाल बॉक्स की ओर इशारा करते हैं और कहते हैं, "हाँ, बिल्कुल यहाँ!" बिना खाना पकाए।

यह एक बड़ी बात क्यों है?

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

ट्रेड-ऑफ (एक "कैच")

पेपर एक सीमा को स्वीकार करता है: आपको नियम पहले से पता होने चाहिए।
रेस्टोरेंट की उपमा में, आपको पेंट्री व्यवस्थित करने से पहले ही पता होना चाहिए कि आप किन सामग्रियों का उपयोग कर रहे हैं। यदि कोई ग्राहक अचानक एक बिल्कुल नया, अजीब घटक लेकर आता है जिसके बारे में आप नहीं जानते थे, तो आपको रुकना होगा और पूरी पेंट्री को फिर से व्यवस्थित करना होगा।

हालांतु, अधिकांश वास्तविक दुनिया की समस्याओं के लिए जहाँ नियम ज्ञात होते हैं, यह दृष्टिकोण गेम-चेंजर है। यह एक "कठिन गणित की समस्या" को "सरल लुकअप समस्या" में बदल देता है।

एक वाक्य में सारांश

यह पेपर कंप्यूटर को गणित के सभी नियमों को पहले से कैलकुलेट करने और उन्हें एक विशेष, सुपर-फास्ट लॉजिक फॉर्मेट में पिरोने का तरीका सिखाता है, ताकि बाद में जटिल प्रश्नों के उत्तर देना लाइट स्विच चालू करने जितना आसान हो जाए।

यहाँ शोध पत्र "d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

नॉलेज कंपाइलेशन (Knowledge Compilation - KC) एक ऐसा प्रतिमान (paradigm) है जहाँ एक प्रपोज़िशनल नॉलेज बेस को ऑफलाइन रूप से एक लक्षित रूप (आमतौर पर deterministic decomposable negation normal form, या d-DNNF) में संकलित (compile) किया जाता है ताकि ऑनलाइन प्रश्नों (जैसे, मॉडल काउंटिंग, एंटेलमेंट, वैलिडिटी) को बहुपद समय (polynomial time) में उत्तर दिया जा सके।

हालाँकि, मौजूदा KC तकनीकें काफी हद तक प्रपोज़िशनल (propositional) डोमेन तक ही सीमित हैं। इन तकनीकों को सैटिस्फिएबिलिटी modulo theories (SMT) तक विस्तारित करना चुनौतीपूर्ण है क्योंकि:

थ्योरी इनकंसिस्टेंसी (Theory Inconsistency): SMT में, एटम्स (atoms) के लिए एक प्रपोज़िशनल असाइनमेंट प्रपोज़िशनल रूप से सुसंगत हो सकता है लेकिन बैकग्राउंड थ्योरी $T$ के संबंध में असंगत हो सकता है (जैसे, $x \le 0$ और $x \ge 1$ )। मानक d-DNNF कंपाइलेशन स्वाभाविक रूप से इन $T$ -असंगत असाइनमेंट्स को फ़िल्टर नहीं करता है।
क्वेरी कॉम्प्लेक्सिटी (Query Complexity): बिना फ़िल्टरिंग के, संकलित d-DNNF पर मानक प्रपोज़िशनल क्वेरीज़ SMT समस्याओं के लिए गलत परिणाम देती हैं (जैसे, उन मॉडल्स की गिनती करना जो सैद्धांतिक रूप से असंभव हैं)।
लेज़ी अप्रोच की सीमाएँ (Limitations of Lazy Approaches): SMT सॉल्वर में उपयोग किए जाने वाले मानक "लेज़ी" लेम्मा-ऑन-डिमांड (lemma-on-demand) दृष्टिकोण का उपयोग KC के लिए उपयुक्त नहीं है। KC के लिए संकलित संरचना का स्व-निहित (self-contained) होना आवश्यक है ताकि सभी आगामी क्वेरीज़ तेज़ हों; क्वेरी चरण के दौरान लेज़ी जनरेशन पर निर्भर रहने से बहुपद-समय (polynomial-time) का आश्वासन नष्ट हो जाएगा।

मूल समस्या यह है: हम एक SMT फॉर्मूला को d-DNNF में कैसे संकलित कर सकते हैं ताकि मानक प्रपोज़िशनल क्वेरीज़ जटिल SMT क्वेरीज़ का सही उत्तर बहुपद समय में दे सकें?

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

लेखक एक नया ढांचा प्रस्तावित करते हैं जो थ्योरी रीजनिंग के कम्प्यूटेशनल बोझ को पूरी तरह से ऑफलाइन कंपाइलेशन चरण पर स्थानांतरित कर देता है। यह कार्यप्रणाली तीन मुख्य स्तंभों पर आधारित है:

A. थ्योरी लेम्मा और "ईगर" कंपाइलेशन (Theory Lemmas and "Eager" Compilation)

लेज़ी जनरेशन के बजाय, यह ढांचा कंपाइलेशन से पहले पूर्व-निर्धारित थ्योरी लेम्मास (थ्योरी $T$ में मान्य क्लॉज़) के एक सेट को ईगरली (eagerly) उत्पन्न करता है। इन लेम्मास को इनपुट फॉर्मूला के साथ जोड़ा जाता है ताकि सभी $T$ -असंगत सत्य असाइनमेंट्स को बाहर निकाला जा सके।

तंत्र (Mechanism): इनपुट SMT फॉर्मूला $\phi$ को एक थ्योरी-लेम्मा एन्यूमिरेटर से प्राप्त लेम्मास $\{C_i\}$ के सेट के साथ बढ़ाया जाता है।
परिणाम: संवर्धित (augmented) फॉर्मूला $T$ -रिड्यूस्ड (T-reduced) (सैटिस्फिएबिलिटी/काउंटिंग क्वेरीज़ के लिए) या $T$ -एक्सटेंडेड (T-extended) (वैलिडिटी/इम्प्लिकेंट क्वेरीज़ के लिए) हो जाता है।
- एक फॉर्मूला $T$ -रिड्यूस्ड है यदि इसके सभी प्रपोज़िशनल संतुष्ट करने वाले असाइनमेंट्स भी $T$ -संतुष्ट (T-satisfiable) हैं।
- एक फॉर्मूला $T$ -एक्सटेंडेड है यदि इसके सभी प्रपोज़िशनल असंतुष्ट करने वाले असाइनमेंट्स भी $T$ -असंतुष्ट (T-falsifying) हैं।

B. प्रपोज़िशनल क्वेरीज़ में न्यूनीकरण (Reduction to Propositional Queries)

यह शोध पत्र सिद्ध करता है कि यदि एक d-DNNF $T$ -रिड्यूस्ड या $T$ -एक्सटेंडेड है, तो जटिल SMT क्वेरीज़ को उनके प्रपोज़िशनल समकक्षों में बदला जा सकता है:

$T$ -रिड्यूस्ड d-DNNFs के लिए:
- $T$ -कंसिस्टेंसी (CO), क्लॉज़ एंटेलमेंट (CE), मॉडल काउंटिंग (MC/#SMT), और मॉडल एन्यूमरेशन (ME/AllSMT) को मानक प्रपोज़िशनल d-DNNF रीज़नर का उपयोग करके बहुपद समय में कंप्यूट किया जा सकता है।
$T$ -एक्सटेंडेड d-DNNFs के लिए:
- $T$ -वैलिडिटी (VA) और इम्प्लिकेंट चेक (IM) को बहुपद समय में कंप्यूट किया जा सकता है।
इक्विवेलेंस (EQ) और सेंटेंशियल एंटेलमेंट (SE): OBDDs और SDDs जैसे कैनोनिकल रूपों के लिए, ये जाँच भी बहुपद-समय प्रपोज़िशनल जाँच में बदल जाती है।

C. अतिरिक्त एटम्स को संभालना (Handling Extra Atoms)

यह ढांचा उन SMT सॉल्वर्स को ध्यान में रखता है जो सहायक एटम्स (auxiliary atoms) पेश करते हैं (जैसे, लीनियर अरिथमेटिक या थ्योरी कॉम्बिनेशन के लिए)। लेखक लीनियर अरिथमेटिक के लिए लेम्मा जनरेशन को इन अतिरिक्त एटम्स को संभालने के लिए सामान्य बनाते हैं, जिससे उन्हें बूलियन एब्स्ट्रैक्शन के कंपाइलेशन के दौरान अस्तित्वगत क्वांटिफिकेशन (existentially quantify) के माध्यम से बाहर निकाला जा सके, जिससे अंतिम d-DNNF केवल मूल एटम्स पर निर्भर रहे।

D. कार्यान्वयन रणनीति (Implementation Strategy)

इस ढांचे को एक पाइपलाइन के रूप में लागू किया गया है:

लेम्मा एन्यूमरेशन: आवश्यक $T$ -लेम्मास उत्पन्न करने के लिए एक थ्योरी-एग्नोस्टिक लेम्मा एन्यूमिरेटर (पूर्व कार्य [9] पर आधारित) का उपयोग करें।
ऑगमेंटेशन (Augmentation): इन लेम्मास को मूल फॉर्मूला के साथ जोड़ें (T-रिड्यूस्ड के लिए) या विलीन करें (T-एक्सटेंडेड के लिए)।
कंपाइलेशन: संवर्धित फॉर्मूला के बूलियन एब्स्ट्रैक्शन को एक मानक प्रपोज़िशनल d-DNNF कंपाइलर (जैसे, D4, CUDD, PYSDD) में फीड करें।
क्वेरीइंग: संकलित संरचना पर क्वेरी का उत्तर देने के लिए एक मानक प्रपोज़िशनल d-DNNF रीज़नर का उपयोग करें।

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

प्रथम सामान्य ढांचा: यह सामान्य d-DNNF कंपाइलेशन और क्वेरीइंग को SMT स्तर तक सफलतापूर्वक विस्तारित करने वाला पहला कार्य है, जो किसी भी थ्योरी या थ्योरी कॉम्बिनेशन का समर्थन करता है।
सैद्धांतिक गारंटी: लेखकों ने $T$ -रिड्यूस्ड और $T$ -एक्सटेंडेड फॉर्मूला को औपचारिक रूप से परिभाषित किया है और सिद्ध किया है कि ये गुण बहुपद-समय जटिलता को बनाए रखते हुए SMT क्वेरीज़ को प्रपोज़िशनल क्वेरीज़ में बदलने की अनुमति देते हैं।
ब्लैक-बॉक्स मोडुलैरिटी: यह दृष्टिकोण मॉड्यूलर है। यह किसी भी मौजूदा d-DNNF कंपाइलर और किसी भी थ्योरी-लेम्मा एन्यूमिरेटर के साथ काम करता है, उन्हें ब्लैक बॉक्स के रूप में मानता है।
कैनोनिकल एक्सटेंशन: यह ढांचा कैनोनिकल रूपों (OBDDs, SDDs) तक विस्तृत है, जिससे SMT फॉर्मूला के लिए बहुपद-समय इक्विलिवेलेंस और एंटेलमेंट जाँच संभव होती है, जो पहले विशिष्ट थ्योरीज या प्रतिबंधित प्रारूपों तक सीमित थी।
प्रोटोटाइप टूल: लेखकों ने अत्याधुनिक d-DNNF पैकेज (D4, CUDD, PYSDD) और एक नए लेम्मा एन्यूमिरेटर को एकीकृत करने वाला एक प्रोटोटाइप टूल बनाया, जो इस दृष्टिकोण की व्यवहार्यता को प्रदर्शित करता है।

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

लेखकों ने 450 सिंथेटिक SMT(LRA) इंस्टेंस पर अपने दृष्टिकोण का मूल्यांकन किया, अपने संकलित d-DNNFs की तुलना मानक SMT सॉल्वर (MathSAT5) और AllSMT एन्यूमरेशन से की।

कंपाइलेशन समय (Compilation Time):
- d-DNNFs के लिए कंपाइलेशन में लेम्मा एन्यूमरेशन चरण हावी रहता है, जबकि OBDDs/SDDs के लिए बूलियन कंपाइलेशन हावी रहता है।
- d-DNNFs ने कम संरचनात्मक बाधाओं के कारण OBDDs/SDDs की तुलना में काफी अधिक इंस्टेंस और तेज़ी से संकलित किए।
प्रतिनिधित्व आकार (Representation Size):
- आश्चर्यजनक रूप से, थ्योरी लेम्मास जोड़ने से संकलित प्रतिनिधित्व का आकार नहीं बढ़ा; कई मामलों में, संकलित d-DNNFs इनपुट फॉर्मूला से भी छोटे थे।
क्वेरी प्रदर्शन (Query Performance):
- क्लॉज़ल एंटेलमेंट (CE): संकलित d-DNNFs ने नॉन-इन्क्रीमेंटल SMT की तुलना में बहुत बेहतर प्रदर्शन किया और वे आम तौर पर इंक्रीमेंटल SMT से तेज़ थे।
- मॉडल काउंटिंग (#SMT): यह सबसे महत्वपूर्ण जीत थी। मानक AllSMT एन्यूमरेशन अधिकांश क्वेरीज़ को समय सीमा के भीतर हल करने में विफल रहा। इसके विपरीत, $T$ -रिड्यूस्ड d-DNNF ने सभी क्वेरीज़ को एक सेकंड के अंश में (संकलित आकार के सापेक्ष रैखिक समय में) हल किया।
- स्केलेबिलिटी: यह दृष्टिकोण कई महंगे प्रश्नों पर उच्च लागत को प्रभावी ढंग से कम (amortize) करता है, जिससे पहले अगम्य (intractable) SMT काउंटिंग समस्याएं भी हल करने योग्य बन जाती हैं।

5. महत्व (Significance)

यह शोध पत्र नॉलेज कंपाइलेशन सिद्धांतों को थ्योरी स्तर पर लागू करके SMT सॉल्विंग में एक प्रतिमान परिवर्तन (paradigm shift) का प्रतिनिधित्व करता है।

दक्षता (Efficiency): यह ऑफलाइन कंपाइलेशन चरण के बाद घातांकीय-समय (exponential-time) SMT क्वेरीज़ (जैसे, मॉडल काउंटिंग) को बहुपद-समय ऑपरेशन्स में बदल देता है।
सामान्यीकरण (Generality): विशिष्ट थ्योरीज (जैसे, लीनियर अरिथमेटिक) या विशिष्ट प्रारूपों (जैसे, OBDDs) तक सीमित पिछले कार्यों के विपरीत, यह ढांचा थ्योरी-एग्नोस्टिक है और सभी d-DNNF वेरिएंट्स का समर्थन करता है।
व्यावहारिक प्रभाव: यह कुशल SMT-आधारित सत्यापन और विश्लेषण कार्यों के द्वार खोलता है जिनमें बार-बार क्वेरीज़ की आवश्यकता होती है, जैसे कि प्रोबेबिलिस्टिक रीजनिंग, रिलायबिलिटी एनालिसिस, और जटिल सिस्टम का फॉर्मल वेरिफिकेशन, जहाँ वर्तमान SMT सॉल्वर बार-बार काउंटिंग या एन्यूमरेशन के मामले में संघर्ष करते हैं।

सीमाएँ और भविष्य का कार्य:
वर्तमान दृष्टिकोण के लिए कंपाइलेशन के समय एटम्स का ज्ञात होना आवश्यक है। भविष्य के कार्य में लेम्मा जनरेशन और d-DNNF कंपाइलेशन के लिए इंक्रीमेंटल तकनीक विकसित करने का लक्ष्य है ताकि डायनेमिक एटम सेट्स को संभाला जा सके।