समीकरण को समझने

Question

समीकरण पेल x*x - 193 * y*y = 1

z3py में

है की आवश्यकता है:

x = BitVec('x',64) 
y = BitVec('y',64) 
solve(x*x - 193 * y*y == 1, x > 0, y > 0) 

परिणाम: [y = 2744248620923429728, x = 8169167793018974721]

क्यों?

पीएस वैध उत्तर: [वाई = 448036604040, एक्स = 6224323426849]

Answer 1

डायफोंटाइन समीकरणों को हल करने के लिए बिट-वेक्टर अंकगणित का उपयोग करना संभव है। पैड द्वारा उल्लिखित ओवरफ्लो से बचने के लिए ZeroExt का उपयोग करना मूलभूत विचार है। उदाहरण के लिए, यदि हम दो बिट-वेक्टर x और y आकार n के गुणा कर रहे हैं, तो हमें n शून्य बिट्स x और y में यह सुनिश्चित करने के लिए जोड़ना होगा कि परिणाम अधिक नहीं होगा। यही कारण है, हम लिखते हैं:

ZeroExt(n, x) * ZeroExt(n, y) 

अजगर कार्यों के निम्नलिखित सेट "सुरक्षित रूप से" बिट-वेक्टर गणित में किसी भी Diophantine समीकरण D(x_1, ..., x_n) = 0 एन्कोड करने के लिए इस्तेमाल किया जा सकता। "सुरक्षित रूप से" से मेरा मतलब है कि अगर कोई समाधान है जो x_1, ..., x_n को एन्कोड करने के लिए उपयोग की जाने वाली बिट्स की संख्या में फिट बैठता है, तो अंत में यह स्मृति और समय जैसे मॉड्यूल संसाधनों को मिलेगा। इन फ़ंक्शंस का उपयोग करके, हम पेल के समीकरण x^2 - d*y^2 == 1 को eq(mul(x, x), add(val(1), mul(val(d), mul(y, y)))) के रूप में एन्कोड कर सकते हैं। pell(d,n) और y के लिए n बिट्स का उपयोग करने के लिए मान खोजने का प्रयास करता है। http://rise4fun.com/Z3Py/Pehp

कहा जा रहा है, यह बिट-वेक्टर अंकगणित का प्रयोग कर पेल के समीकरण को हल करने के लिए सुपर महंगा है:

नीचे दिए गए लिंक पूर्ण उदाहरण में शामिल है। समस्या यह है कि बिट-वेक्टर सॉल्वर के लिए गुणा वास्तव में कठिन है। Z3 द्वारा उपयोग किए जाने वाले एन्कोडिंग की जटिलता n पर वर्गबद्ध है। मेरी मशीन पर, मैंने केवल पेल के समीकरणों को हल करने में कामयाब रहे जिनमें छोटे समाधान हैं। उदाहरण: d = 982, d = 980, d = 1000, d = 1001। सभी मामलों में, मैंने 24 से छोटा उपयोग किया था। मुझे लगता है कि d = 991 जैसे बहुत कम न्यूनतम सकारात्मक समाधानों के साथ समीकरणों की कोई उम्मीद नहीं है, जहां हमें x और y के मानों को एन्कोड करने के लिए लगभग 100 बिट्स की आवश्यकता है। इन मामलों के लिए, मुझे लगता है कि एक विशेष सॉल्वर बहुत बेहतर प्रदर्शन करेगा।

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

def mul(x, y): 
    sz1 = x.sort().size() 
    sz2 = y.sort().size() 
    return ZeroExt(sz2, x) * ZeroExt(sz1, y) 
def add(x, y): 
    sz1 = x.sort().size() 
    sz2 = y.sort().size() 
    rsz = max(sz1, sz2) + 1 
    return ZeroExt(rsz - sz1, x) + ZeroExt(rsz - sz2, y) 
def eq(x, y): 
    sz1 = x.sort().size() 
    sz2 = y.sort().size() 
    rsz = max(sz1, sz2) 
    return ZeroExt(rsz - sz1, x) == ZeroExt(rsz - sz2, y) 
def num_bits(n): 
    assert(n >= 0) 
    r = 0 
    while n > 0: 
    r = r + 1 
    n = n/2 
    if r == 0: 
    return 1 
    return r 
def val(x): 
    return BitVecVal(x, num_bits(x)) 
def pell(d, n): 
    x = BitVec('x', n) 
    y = BitVec('y', n) 
    solve(eq(mul(x,x), add(val(1), mul(val(d), mul(y, y)))) , x > 0, y > 0)