z3実数累乗

Question

私は奇妙な状況に遭遇しました。ここでは、z3pyは論理的に同じ問題になる2つの別々の答えを出します。

バージョン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 

バージョン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 

がどのように私はそれが正確な結果を生成するように、バージョン1でやって変更するのですか？これらの制約はオンザフライで生成されており、オンザフライで再書き込みを試みる場合、アプリケーションの複雑さを大幅に増やす可能性があります。また、ルートが本当にシンボリックである場合、単にPython自体がその問題を解決することはできません。

編集：私は、私は私のソルバーのために次の設定を使用している場合、それは（少し遅くなるが）成功し解決することを発見しました：

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

それは意味合いがであるか私には完全には明らかではありませんただし、デフォルトソルバではなく、それを指定します。

Answer 1

非線形の実際の問題に対するZ3の性能はあまり良くありませんが、必要なすべてのソリューションを見つけるためには間違いなく手間がかかります。私の最初の試みは、常にNLSATソルバーに切り替えることです（qfnra-nlsatの戦術を適用するか、ソルバーを作ってください）。そのソルバーはQF_NRAの問題ではるかに優れていますが、他のタイプの変数を持っている場合には、理論的な組み合わせはサポートされません。

また、「Z3」と「非線形」についてのstackoverflowを検索すると、そのさまざまな側面について多数の質問と回答がありました。