z3 Real Exponentiation

Question

Z3py'nin mantıksal olarak aynı sorun için iki ayrı yanıt ürettiği garip bir durumla karşılaşıyorum.

Versiyon 1:

>>> import z3 
>>> r, r2, q = z3.Reals('r r2 q') 
>>> s = z3.Solver() 
>>> s.add(r > 2, r2 == r, q == r2 ** z3.RealVal(0.5)) 
>>> s.check() 
unknown 

Versiyon 2

>>> import z3 
>>> r, r2, q = z3.Reals('r r2 q') 
>>> s = z3.Solver() 
>>> s.add(r > 2, r2 == r, q * q == r2) 
>>> s.check() 
sat 

nasıl bunu doğru bir sonuç üretecektir böylece sürüm 1 ile ne yapıyorum değiştirebilirim? Bu kısıtlamalar anında oluşturulmakta ve anında yeniden yazmayı denemek istiyorsam uygulamanın karmaşıklığına büyük ölçüde katkıda bulunacaktır. Ayrıca, kökün gerçekten sembolik olduğu durumda, Python'un kendisi için bu sorunu çözmesi mümkün olmazdı.

Düzenleme: (biraz daha yavaş olsa da) benim Çözücü için aşağıdaki kurulumunda, başarıyla çözecek olduğunu keşfettim:

z3.Then("simplify","solve-eqs","smt").solver() 

Bana tamamen net değil etkileri arasında ne Ancak, sadece varsayılan çözücüden ziyade, bunu belirterek.

Answer 1

Doğrusal olmayan gerçek problemler üzerindeki Z3'ün kutu performansının dışında, büyük bir olasılıkla, ihtiyacınız olan tüm çözümleri bulmasını sağlamak için biraz uğraşacaksınız. İlk denemem her zaman NLSAT çözücüye geçmek (qfnra-nlsat taktiğini uygulamak veya çözücü yapmak). Bu çözücü, QF_NRA problemlerinde genellikle çok daha iyidir, ancak herhangi bir teori kombinasyonunu desteklemez, yani, başka değişken türleriniz varsa, kurtarılacaktır. Ayrıca, "Z3" ve "doğrusal olmayan" için de yığın akışını araştırın, çeşitli açılardan çok sayıda soru ve cevaplar vardır.