問題タブ [groebner-basis]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
python - 3 次多項式の系を解く (ベジエ曲線の交点を見つけるため)
このシステムの解決策を見つけるための修正または代替ルートを提案できる人はいますか? 特に、[0,1]x[0,1] の解 (s,t) のみを気にします
注: ここでは、2 つの 3 次ベジエ曲線の交点を探しています。メソッドがすべてのソリューションを確実に見つけられるようにする必要があり、できれば妥当な時間内に実行する必要があります (私の使用では、これは曲線のペアごとに数秒を意味します)。
sympy を使用してみましたが、solve() と solve_poly_system() の両方が空のリストを返しました。
これが私のコードです：
これは以下を出力します:
読んでくれてありがとう！
timeout - 算術サブソルバーで費やされた時間を測定してバインドする
Q1: Z3 がさまざまなサブソルバーで費やした時間を照会することは可能ですか?
呼び出し(get-info :all-statistics)により、Z3 の全体的な実行時間が得られますが、個々のサブソルバーに分解したいと思います。
特に、算術関連のサブソルバーに費やされた時間、より正確には、統計grobnerとnonlinear-horner.
Q2:また、サブソルバーにタイムアウトを付けることは可能ですか?
チェックサットとサブソルバーごとにタイムアウトを定義して、Z3 がそのサブソルバーで費やすことができる時間を制限するようなものを想像できます。Z3 はn 個の異なるサブソルバーを繰り返し呼び出し、そのうちの 1 つの時間制限に達した場合は続行しますが、残りのn-1サブソルバーのみを使用します。
戦術のチュートリアルを読んで、これは実際には次のような方法で可能であるという印象を受けました。
しかし、どのソルバーを使用すればよいかわかりませんでした。
z3 - (構文上の) 等価性の推論に対する smt.arith.nl.gb の予期しない影響 - バグ?
次の SMTLIB プログラムを検討してください (rise4fun here で):
Z3 (4.3.2 公式リリース、および 4.4.0 b6c40c6c0eaf) は、構文上の同等性に関する推論のみを必要とするように見えますが、最終的なアサーションが であることを示していませんunsat。
予想外に（少なくとも私にとっては）、に設定smt.arith.nl.gbするtrueと、例が検証されます（つまり、check-satyields unsat）。
それだけの価値があるため、さらにいくつかの観察結果を次に示します。
乗算がまたはにそれぞれ変更された場合、最終的なアサーションを示すことができます。
unsat(* i n)(* n i)乗算を次のように変更すると表示できません。
unsat(* i i)(push)例に(pop)影響を与えるようには見えません。つまり、記述された観察に影響を与えずに削除できます。
smt.arith.nl.gbこれはバグですか、それともこの例を表示する必要がある理由はありunsatますか?
computational-geometry - グレブナー基底で定理を証明する
Groebner Basis を使用していくつかの定理を証明しようとしています (Cox、Little、O'Shea Linkで説明されているように )
言及された本は、与えられた方法論を使用してパップスの定理を証明するための演習として与えられていますが、私は実際にそれを機能させることはできません. Sage、Mathematica、および Singular を使用してみましたが、Grobner Basis の計算が終了しません。
私に何ができるか考えていますか？他の誰かが以前にこのエクササイズをしたことがありますか? ありがとう。
これは特異なコードです: