क्या मैं z3 में बूलियन चर की प्राथमिकता निर्धारित कर सकता हूं?

Question

चूंकि सवाल वर्णन करने में थोड़ा मुश्किल है, इसलिए मैं अपने प्रश्न का वर्णन करने के लिए एक छोटा सा उदाहरण उपयोग करूंगा। मान लीजिए कि एक प्रस्तावक सूत्र सेट है जिसका तत्व बूलियन चर ए, बी और सी हैं। इस सूत्र सेट के सच्चे असाइनमेंट के लिए z3 का उपयोग करते समय, चर की प्राथमिकता निर्धारित करने के लिए कोई तरीका मौजूद है? मेरा मतलब है कि अगर प्राथमिकता एक> बी> सी है, तो खोज प्रक्रिया के दौरान z3 सबसे पहले मान लेता है कि यह सत्य है और यदि कोई सच होना असंभव है तो यह मानता है कि बी सत्य है और इसी तरह। दूसरे शब्दों में, यदि z3 एक सत्य असाइनमेंट देता है: ए, बी, सी उपर्युक्त प्राथमिकता के तहत नहीं है, इसका मतलब है कि यह सच होना असंभव है क्योंकि बी की तुलना में उच्च प्राथमिकता है। उम्मीद है कि मैं स्पष्ट रूप से प्रश्न का वर्णन करता हूं।

Answer 1

वर्तमान रिलीज में इसे करने का कोई आसान तरीका नहीं है (v4.3.1)। एकमात्र तरीका मैं देख सकता हूं कि Z3 स्रोत कोड (http://z3.codeplex.com) हैक/संशोधित करना है। हम मानते हैं कि प्राथमिकताओं को सेट करना कुछ अनुप्रयोगों के लिए उपयोगी सुविधा है, हालांकि कुछ समस्याएं हैं।

सबसे पहले, Z3 किसी समस्या को हल करने से पहले कई परिवर्तन (उर्फ प्रीप्रोकैसिंग चरण) लागू करता है। चर बनाया और समाप्त कर रहे हैं। इस प्रकार, मूल समस्या के लिए एक केस-स्प्लिट प्राथमिकता वास्तविक समस्या (जेड 3 द्वारा हल किए गए सभी परिवर्तनों को लागू करने के बाद उत्पन्न) के लिए व्यर्थ हो सकती है।

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

जेड 3 सॉल्वर और प्रीप्रोसेसरों का संग्रह है। डिफ़ॉल्ट रूप से, Z3 उपयोगकर्ता के लिए स्वचालित रूप से एक सॉल्वर का चयन करेगा। इनमें से कुछ हलकर्ता पूरी तरह से अलग एल्गोरिदम का उपयोग करते हैं। इसलिए, प्रदत्त प्राथमिकता का उपयोग करने वाले सॉल्वर के लिए बेकार हो सकता है।

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