एसएमटी सॉल्वर की सीमा

Question

परंपरागत रूप से कम्प्यूटेशनल तर्क के साथ अधिकांश काम या तो प्रस्ताव था, इस मामले में आपने एक एसएटी (बूलियन संतुष्टि) सॉल्वर या प्रथम क्रम का उपयोग किया था, इस मामले में आपने पहले ऑर्डर प्रमेय प्रोवर का उपयोग किया था।

हाल के वर्षों में, एसएमटी (संतुष्टि मॉड्यूलो सिद्धांत) हलकों पर बहुत सी प्रगति हुई है, जो मूल रूप से अंकगणितीय सिद्धांतों के सिद्धांतों के साथ प्रस्तावपरक तर्क को बढ़ाती है; एसआरआई इंटरनेशनल के जॉन रशबी अब तक एक विघटनकारी तकनीक कहने के लिए जाते हैं।

समस्याओं के सबसे महत्वपूर्ण व्यावहारिक उदाहरण क्या हैं जिन्हें प्रथम क्रम तर्क में संभाला जा सकता है लेकिन फिर भी एसएमटी द्वारा नियंत्रित नहीं किया जा सकता है? सबसे विशेष रूप से, किस प्रकार की समस्याएं उत्पन्न होती हैं जिन्हें सॉफ़्टवेयर सत्यापन के डोमेन में एसएमटी द्वारा नियंत्रित नहीं किया जा सकता है?

Answer 1

एसएमटी सॉल्वर एसएटी सॉल्वर से कहीं ज्यादा शक्तिशाली नहीं हैं। वे अभी भी घातीय समय में चलेंगे या एसएटी में एक ही समस्या के लिए अपूर्ण होंगे। एसएमटी का लाभ यह है कि एसएमटी में स्पष्ट होने वाली कई चीजें एक समकक्ष सैट सॉल्वर को फिर से खोजने में काफी समय लग सकती हैं।

तो उदाहरण के रूप में सॉफ़्टवेयर सत्यापन के साथ, यदि आप एक क्यूएफ बीवी (बिट-वेक्टर के क्वांटिफायर-मुक्त सिद्धांत) एसएमटी सॉल्वर का उपयोग करते हैं, तो एसएमटी सॉल्वर को पता होगा कि एक शब्द पर (ए + बी = बी + ए) इसके बजाय स्तर, जबकि यह एक एसएटी सॉल्वर को साबित करने के लिए वास्तव में लंबा समय ले सकता है कि व्यक्तिगत बुलियन मूल्यों का उपयोग करना।

तो सॉफ़्टवेयर सत्यापन के लिए wrt, आप आसानी से सॉफ़्टवेयर सत्यापन में समस्याएं बना सकते हैं जो कि किसी भी SMT या SAT सॉल्वर के लिए कठिन होगा।

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

दूसरा, सामान्य रूप से कठिन समस्याओं को क्यूएफ बीवी में एन्कोड करना आसान है। उदाहरण के लिए, आप एक प्रोग्राम लिख सकते हैं इस प्रकार है:

void run(int64_t a,int64_t b) 
{ 
    a * b == <some large semiprime>; 

    assert (false); 
} 

अब निश्चित रूप से श्रीमती solver आसानी से ज़ोर साबित होगा (गलत) हो जाएगा, लेकिन यह एक काउंटर उदाहरण प्रदान करना होगा, जो आपको दे देंगे इनपुट a,b। यदि आप <some large number> को आरएसए सेमिप्रिम पर सेट करते हैं, तो आप गुणा को उलट देते हैं ... अन्यथा पूर्णांक कारक के रूप में जाना जाता है! इस प्रकार यह किसी भी एसएमटी सॉल्वर के लिए कठिन होगा, और यह दर्शाता है कि सॉफ्टवेयर सत्यापन सामान्य रूप से एक कठिन समस्या है (जब तक पी = एनपी, या कम से कम पूर्णांक कारककरण आसान हो जाता है)। इस तरह के एसएमटी सॉल्वर एसएटी सॉल्वर पर आसानी से लिखने और आसानी से तर्क के साथ चीजों को ड्रेस करके एसएटी सॉल्वर पर एक पैर ऊपर हैं।

एसएमटी सॉल्वर जो अधिक उन्नत सिद्धांतों को हल करते हैं, वे अपूर्ण हैं या एसएटी सॉल्वर से भी धीमे हैं, क्योंकि वे कठिन समस्याओं को हल करने का प्रयास कर रहे हैं।

यह भी देखें:

• दिलचस्प बात यह है Beaver SMT solver CNF के लिए QF BV तब्दील हो और एक बैक-एंड के रूप में एक सैट solver उपयोग कर सकते हैं।
• Klee जो एक कार्यक्रम LLVM आईआर (मध्यवर्ती प्रतिनिधित्व) का संकलन किया है, और कीड़े के लिए चेक ले जा सकते हैं, और कथनों आदि के लिए काउंटर उदाहरण पाता है यह एक बग मिलते हैं तो वह (शुद्धता के लिए एक काउंटर उदाहरण दे सकता हूँ कहीं भी होगी आपको इनपुट दें जो बग को पुन: पेश करेगा)।