Z3にパワーモイド演算を実行できますか?例えば、私が並べ替えx ** y % z
の式に置いている場合、Pythonにどのように関数pow(x,y,z)
があるのと同様に、このタイプの式であることをZ3に伝える方法はありますか?私の前提は、(モジュラ逆数のような)オプションを解くことができるということです。Z3パワーモジュロステートメント
0
A
答えて
0
興味深い点。これは特にZ3ではサポートされていません。この分野で知られている技術は何ですか?
+0
私は技術を理解していることは間違いありません。学部修学生の数年を経て、私はそのような問題のクラスを簡素化するためにその時にいくつかの技術を思い出しています。私が言うことから、Z3に直接記述されているpowmodは、解決のために非常に資源集中的です。 –
+0
与えられた* x *と* y *を計算する順方向については、べき乗剰余算法は非常に効率的であり、通常、* x * mod * z *を二乗法* x^y * mod * z *を構築する* y *の分解。 * x *と* z *を指定した* y *を見つける逆の問題は、離散対数問題です。だから、Z3や他の誰にとっても難しいです。 –
関連する問題
- 1. z3 :: tacticとz3 :: goalの目的
- 2. Z3セグメンテーションフォールト
- 3. z3 C++ API&ite
- 4. Z3のセグメンテーションフォルトSMT
- 5. Z3コンテキストのシリアライズ/デシリアライズ?
- 6. Z3 QBVFの質問
- 7. Z3ファイルを読む
- 8. Z3/Pythonの実数
- 9. z3 timeout on linux/mac
- 10. z3実数累乗
- 11. Z3 Z3をSATソルバーとして使用する極性
- 12. z3バイナリとz3 apiの結果が異なります
- 13. z3にリスケートを表示
- 14. 奇妙なZ3モデル値
- 15. z3の関数宣言
- 16. Z3とcoqの相違
- 17. Z3定量器のサポート
- 18. Z3のソフト/ハード制約
- 19. Z3の反例出力例
- 20. 現在のバージョンよりz3
- 21. z3から間違った結果
- 22. Z3の初期モデル値の指定
- 23. SMTLIBアレイ理論Z3の奇妙さ
- 24. WindowsでScala^Z3をコンパイルする
- 25. z3モデルの配列用語の値
- 26. Z3モデルが正しくない
- 27. Z3 INIオプションの詳細な文書
- 28. Z3またはZ3Pyの前提
- 29. Z3での除外と組み込み
- 30. Z3はCraig補間をサポートします
Z3がその種の計算を特別にサポートしているかどうかを確認するだけですか?それとも解決策を求めていますか?満たされていないことを証明することに興味があれば、定量化された式としていくつかのpow-modルールをZ3に提供することができます。 – iago
私の質問の根拠は、それらの文を入力する良い方法があるのでしょうか?入力として、彼らは戻って非常に長い時間がかかります。残念ながら、私は実際に自分自身で問題を実際に助けるために数学の側(またはその問題のコーディング側)で十分にスマートではありません。答えのように聞こえるのは、今のところ、上記のやり方が正しいことだということです。 –
Z3はpow-modを特別にサポートしていないので、Z3を使ったpow-modに関連する問題を効率的に処理できないわけではありません。しかし、これはあなたの側でいくつかの前処理とエンコーディングトリックを必要とするかもしれません。具体的な問題の例を提示した場合、具体的なソリューション例について議論することもできます。 – iago