Z3 में TryFor दिए गए timelimit

Question

के बाद जांचना बंद नहीं करता है मैं Z3 के .NET API का उपयोग कर रहा हूं। जब मैं फोन करके एक solver का दृष्टांत:

Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit)); 

और बयान

s.Check() 

60 सेकंड के बाद वापस नहीं करता है कुछ मॉडलों के लिए यह 60 सेकंड (60000 मिलीसेकंड) के एक Timelimit दे। कुछ मॉडलों के लिए यह कुछ सेकंड बाद लौटाता है, जो मेरे मामले में कोई समस्या नहीं होगी, लेकिन कुछ मॉडलों के लिए यह बिल्कुल वापस नहीं आता है (मैंने 3 दिनों के बाद प्रक्रिया रद्द कर दी है)।

मैं किसी दिए गए समय-सारणी के बाद जांचने के लिए Z3 को कैसे रोक सकता हूं?

Answer 1

TryFor संयोजक "रद्दीकरण" ध्वज का उपयोग करके लागू किया गया है। नई रणनीति बहुत प्रतिक्रियाशील होती है, और "रद्दीकरण" ध्वज सेट होने पर बहुत तेज़ी से समाप्त हो जाती है। दुर्भाग्यवश, सामान्य उद्देश्य रणनीति smt एक सामान्य प्रयोजन सॉल्वर पर एक रैपर है। यह सामान्य उद्देश्य सॉल्वर बहुत ही संवेदनशील नहीं है। यह कई महत्वपूर्ण स्थानों में "खो गया" प्राप्त कर सकता है: क्वांटिफायर इंस्टेंटेशन, सिंपलक्स इत्यादि। qflia रणनीति smt और कई अन्य रणनीति के शीर्ष पर बनाई गई है। चूंकि, आप क्वांटिफायर-मुक्त समस्याओं को हल करने की कोशिश कर रहे हैं। मुझे लगता है कि smt रणनीति सिम्पलक्स मॉड्यूल के अंदर एक लूप में है। smt रणनीति में सिंपलक्स मॉड्यूल मनमाने ढंग से सटीक तर्कसंगत संख्याओं का उपयोग करके कार्यान्वित किया जाता है। इस प्रकार, यह गैर-तुच्छ रैखिक वास्तविक/पूर्णांक समस्याओं के लिए बहुत समय ले सकता है।

इस मुद्दे को हल करने के लिए आप इतना कुछ नहीं कर सकते हैं। यदि आपको वास्तव में चलने वाले समय में एक मजबूत गारंटी की आवश्यकता है, तो मुझे लगता है कि एकमात्र समाधान Z3 चलाने वाली एक अलग प्रक्रिया बनाना है, और जब भी समस्या हल करने के लिए k सेकंड लेते हैं तो इसे मार दें।

कहा जा रहा है कि, Z3 के भविष्य के संस्करणों में एक पूर्ण नया अंकगणितीय मॉड्यूल होगा। रद्दीकरण ध्वज सेट होने पर यह नया मॉड्यूल (नई रणनीति की तरह) जल्दी समाप्त हो जाएगा।