क्वांटिफायर और पैटर्न (क्यूबीएफ फॉर्मूला)

Question

मैं z3 के लिए smt-lib 2 वाक्यविन्यास में एक क्यूबीएफ एन्कोड करने की कोशिश कर रहा हूं। एक चेतावनी

चेतावनी में z3 परिणाम चल रहा है: परिमाणक के लिए एक पैटर्न खोजने में असफल (! परिमाणक आईडी: k 14)

और satisfiability परिणाम "अज्ञात" है।

(declare-fun R (Bool Bool Bool Bool) Bool) 
(assert 
    (forall ((x2 Bool) (x3 Bool)) 
    (exists ((y Bool)) 
     (forall ((x1 Bool)) 
     (R x1 x2 x3 y) 
    ) 
    ) 
) 
) 
(check-sat) 

मैं बैठ गया-क्वेरी के लिए

(set-option :auto-config false) 
(set-option :mbqi false) 
(declare-fun R (Bool Bool Bool Bool) Bool) 
(declare-fun x1() Bool) 
(declare-fun x2() Bool) 
(declare-fun x3() Bool) 
(declare-fun y() Bool) 
(assert 
    (forall ((x2 Bool) (x3 Bool)) 
    (! 
    (exists ((y Bool)) 
    (! 
     (forall ((x1 Bool)) 
     (! 
     (R x1 x2 x3 y) 
     :pattern((R x1 x2 x3 y))) 
    ) 
    :pattern((R x1 x2 x3 y))) 
    ) 
    :pattern((R x1 x2 x3 y))) 
) 
) 
(check-sat) 

परिणाम के लिए कोड लिख कर चेतावनी से छुटकारा मिला है, तथापि, बनी हुई है "अज्ञात":

कोड इस प्रकार है।

मुझे लगता है कि मुझे पैटर्न सही करने की आवश्यकता है? मैं उन्हें नेस्टेड क्वांटिफायर के लिए कैसे निर्दिष्ट करूं? क्वांटिफायर के साथ सरल उदाहरण पैटर्न एनोटेशन के बिना काम करने लगते हैं, हालांकि।

What is the reason behind the warning message in Z3: "failed to find a pattern for quantifier (quantifier id: k!18) " का जवाब और z3 मार्गदर्शिका ने दुर्भाग्य से मुझे बहुत मदद नहीं की।

Answer 1

इस चेतावनी संदेश को अनदेखा किया जा सकता है। यह सिर्फ आपको सूचित कर रहा है कि ई-मेलिंग इंजन इस मात्राबद्ध सूत्र को संसाधित करने में सक्षम नहीं होगा।

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

डिफ़ॉल्ट कॉन्फ़िगरेशन का उपयोग करके, Z3 आपके उदाहरण के लिए sat वापस करेगा। यह unknown देता है क्योंकि आपने एमबीक्यूआई मॉड्यूल को अक्षम कर दिया है।

एमबीक्यूआई इंजन गारंटी देता है कि जेड 3 कई टुकड़ों के लिए एक निर्णय प्रक्रिया है (http://rise4fun.com/Z3/tutorial/guide देखें)। हालांकि, यह सामान्य रूप से बहुत महंगा है, और जब त्वरित और अनुमानित उत्तर पर्याप्त होते हैं तो उन्हें अक्षम किया जाना चाहिए। इस मामले में, unknown को probably sat के रूप में पढ़ा जा सकता है। सत्यापन उपकरण जैसे कि VCC एमबीक्यूआई मॉड्यूल अक्षम करें क्योंकि यह उनके द्वारा उत्पादित सूत्रों का निर्णय लेने में असमर्थ है। यही है, वीसीसी द्वारा उत्पादित सूत्र एमबीक्यूआई इंजन द्वारा तय किए जा सकने वाले किसी भी टुकड़े में नहीं हैं। हम कहते हैं कि एक टुकड़ा Z3 द्वारा तय किया जा सकता है जब खंड Z3 में किसी भी सूत्र के लिए sat या unsat (यानी, यह unknown वापस नहीं आता है)। बेशक, यह दावा मानता है कि हमारे पास असीमित संसाधन हैं। यही है, ज़ेड 3 भी विफल हो सकता है (यानी, unknown लौटाएं) जब यह स्मृति से बाहर हो जाता है, या उपयोगकर्ता द्वारा टाइमआउट निर्दिष्ट किया गया था तो निर्णायक टुकड़ों के लिए।

अंत में, Z3 3.2 में एमबीक्यूआई इंजन में bug है। बग तय कर दिया गया है, और यह आपकी समस्या को प्रभावित नहीं करता है। यदि आपको आवश्यकता है तो मैं आपको Z3 4.0 का प्री-रिलीज़ संस्करण दे सकता हूं जिसमें बग फिक्स शामिल है।