बिट-वेक्टर अंकगणितीय

Question

के लिए निर्णय प्रक्रियाओं में शब्द पुनर्लेखन का उपयोग मैं एक ऐसे प्रोजेक्ट पर काम कर रहा हूं जिसका फोकस फिक्स्ड-साइज बिट-वेक्टर अंकगणितीय समस्याओं को हल/सरल बनाने के लिए शब्द पुनर्लेखन का उपयोग है, जो कि कुछ करने के लिए उपयोगी है बिट-विस्फोट के आधार पर कुछ निर्णय प्रक्रिया के लिए पहले चरण। शब्द पुनर्लेखन समस्या को हल कर सकता है, या अन्यथा एक बहुत ही सरल समकक्ष समस्या उत्पन्न कर सकता है, इसलिए दोनों के संयोजन के परिणामस्वरूप काफी गति हो सकती है।

मुझे पता है कि कई एसएमटी सॉल्वर इस रणनीति को लागू करते हैं (जैसे बूउलेक्टर, बीवर, ऑल्ट-एर्गो या जेड 3), लेकिन कागजात/तकनीक-रिपोर्ट/आदि ढूंढना मुश्किल है जिसमें इन पुनर्लेखन चरणों का विस्तार से वर्णन किया गया है । आम तौर पर, मुझे केवल कागजात मिलते हैं जिसमें लेखक कुछ अनुच्छेदों में ऐसे सरलीकरण चरणों का वर्णन करते हैं। मैं शब्द पुन: लिखने के उपयोग से विस्तार से कुछ दस्तावेज खोजना चाहता हूं: नियमों के उदाहरण प्रदान करना, एसी पुनर्लेखन और/या अन्य समीकरण सिद्धांतों की सुविधा पर चर्चा करना, पुनर्लेखन रणनीतियों का उपयोग, आदि

अभी के लिए, मैं बस तकनीकी रिपोर्ट A Decision Procedure for Fixed-Width Bit-Vectors मिली है जो सीवीसी लाइट द्वारा किए गए सामान्यीकरण/सरलीकरण चरणों का वर्णन करती है, और मैं इस तरह की अधिक तकनीकी रिपोर्ट ढूंढना चाहता हूं! मुझे Term rewriting in STP के बारे में एक पोस्टर भी मिला है लेकिन यह सिर्फ एक संक्षिप्त सारांश है।

मैं पहले से ही उन श्रीमती समाधानकर्ताओं की वेबसाइटों का दौरा किया है और मैं उनके प्रकाशन पन्नों में खोज की है ...

मैं किसी भी संदर्भ, या कैसे अवधि नए सिरे से लिखना का कोई स्पष्टीकरण नहीं की सराहना करेंगे वर्तमान संस्करण में इस्तेमाल किया जा रहा है प्रसिद्ध एसएमटी solvers के। मैं विशेष रूप से जेड 3 में रूचि रखता हूं क्योंकि ऐसा लगता है कि यह सबसे स्मार्ट सरलीकरण चरणों में से एक है। उदाहरण के लिए, जेड 3 3. * ने एक नई बिट-वेक्टर निर्णय प्रक्रिया शुरू की लेकिन दुर्भाग्यवश, मैं इसका वर्णन करने वाले किसी भी पेपर को खोजने में सक्षम नहीं था।

Answer 1

मैं आपसे सहमत हूँ। आधुनिक एसएमटी सॉल्वर में प्रयुक्त प्रीप्रोकैसिंग चरणों का वर्णन करने वाले कागजात ढूंढना मुश्किल है। अधिकांश एसएमटी सॉल्वर डेवलपर इस बात से सहमत हैं कि बिट-वेक्टर सिद्धांत के लिए ये प्रीप्रोकैसिंग चरण बहुत महत्वपूर्ण हैं। मेरा मानना ​​है कि इन तकनीकों को कई कारणों से प्रकाशित नहीं किया गया है: उनमें से अधिकतर छोटी सी चालें स्वयं एक महत्वपूर्ण वैज्ञानिक योगदान नहीं हैं; अधिकांश तकनीकें केवल एक विशेष प्रणाली के संदर्भ में काम करती हैं; एक तकनीक जो सॉल्वर A पर बहुत अच्छी तरह से काम कर सकती प्रतीत हो सकती है, सोलवर B पर काम नहीं करती है। मेरा मानना ​​है कि ओपन सोर्स एसएमटी सॉल्वर होने के कारण इस मुद्दे को हल करने का एकमात्र तरीका है। यहां तक ​​कि अगर हम किसी विशेष सॉल्वर A में उपयोग की जाने वाली तकनीकों को प्रकाशित करते हैं, तो इसके स्रोत कोड को देखे बिना सॉल्वर ए के वास्तविक व्यवहार को पुन: पेश करना बहुत मुश्किल होगा।

वैसे भी, यहां Z3 द्वारा किए गए प्रीप्रोकैसिंग का सारांश है, और महत्वपूर्ण विवरण।

• कई सरलीकरण नियम, स्थानीय स्तर पर इस आकार को कम कर सकते हैं, लेकिन इसे वैश्विक रूप से बढ़ा सकते हैं। एक सरलीकृत को इस तरह के सरलीकरण के कारण स्मृति ब्लाउप से बचना चाहिए। आप यहां उदाहरण देख सकते हैं: http://research.microsoft.com/en-us/um/people/leonardo/mit2011.pdf

• पहला सरलीकरण चरण केवल स्थानीय सरलीकरण करता है जो समानता को संरक्षित करता है। उदाहरण:

2*x - x -> x 
x and x -> x 

• इसके बाद, जेड 3 निरंतर प्रचार करता है। t = v पर समानता को देखते हुए v एक मान है। यह v के साथ हर जगह t को प्रतिस्थापित करता है।

t = 0 and F[t] -> t = 0 and F[0] 

• इसके बाद, यह बिट-वाहक के लिए गाऊसी उन्मूलन प्रदर्शन करती है। हालांकि, अंकगणितीय अभिव्यक्तियों में सबसे अधिक बार होने वाले केवल वेरिएबल्स समाप्त हो जाते हैं। यह प्रतिबंध आपके सूत्र में योजकों और गुणकों की संख्या में वृद्धि को रोकने के लिए उपयोग किया जाता है। उदाहरण के लिए, मान लें कि हमारे पास x = y+z+w और xp(x+z), p(x+2*z), p(x+3*z) और p(x+4*z) पर होता है। फिर, x को समाप्त करने के बाद, हमारे पास p(y+2*z+w), p(y+3*z+w), p(y+4*z+w) और p(y+5*z+w) होगा। हालांकि हमने x को हटा दिया है, लेकिन हमारे पास मूल सूत्र से अधिक योजक हैं।

• अगला, यह अनियंत्रित चर को समाप्त करता है। इस दृष्टिकोण का वर्णन रॉबर्ट ब्रुमायर और रॉबर्टो ब्रूटोमेसो के पीएचडी थीसिस में किया गया है।

• फिर, सरलीकरण का एक और दौर किया जाता है। इस बार, स्थानीय प्रासंगिक सरलीकरण किया जाता है। ये सरलीकरण संभावित रूप से बहुत महंगा हैं। इसलिए, नोड्स की अधिकतम संख्या पर जाने वाली थ्रेसहोल्ड का उपयोग किया जाता है (डिफ़ॉल्ट मान 10 मिलियन है)। स्थानीय संदर्भ सरलीकरण ऐसे

(x != 0 or y = x+1) -> (x != 0 or y = 1) 

• अगला रूप में नियम होते हैं, यह distributivity का उपयोग कर मल्टीप्लायरों की संख्या को कम करने के लिए प्रयास करता है। उदाहरण:

एक बी + एक ग -> (ब + स) * एक

• फिर, यह संबद्धता लगाने से एडर और मल्टीप्लायरों की संख्या को कम करने की कोशिश करता और कम्यूटिटीविटी। मान लें कि सूत्र में a + (b + c) और a + (b + d) शब्द शामिल हैं। फिर, Z3 उन्हें फिर से लिख देगा: (a+b)+c और (a+b)+d। परिवर्तन से पहले, Z3 को 4 एडर को एन्कोड करना होगा। इसके बाद, Z3 को पूरी तरह से साझा अभिव्यक्तियों का उपयोग करने के बाद केवल तीन एडर को एन्कोड करने की आवश्यकता है।

• यदि सूत्र में केवल समानता, concatenation, निष्कर्षण और इसी तरह के ऑपरेटरों शामिल हैं। फिर, जेड 3 संघ-खोज और एकरूपता बंद करने के आधार पर एक विशेष सॉल्वर का उपयोग करता है।

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

Answer 2

जेड 3 प्री-प्रोसेसिंग के दौरान किए गए कई सरलीकरण के लिए पुनर्लेखन का उपयोग करता है। UFBV रणनीति (परिमाणकों के साथ) के लिए इस्तेमाल किया पुनर्लेखन नियमों से कई निम्नलिखित पत्र में कुछ विस्तार करने के लिए वर्णित हैं:

Wintersteiger, Hamadi, de Moura: Efficiently Solving Quantified Bit-Vector Formulas, FMCAD, 2010