Z3パワーモジュロステートメント

Z3にパワーモイド演算を実行できますか？例えば、私が並べ替えx ** y % zの式に置いている場合、Pythonにどのように関数pow(x,y,z)があるのと同様に、このタイプの式であることをZ3に伝える方法はありますか？私の前提は、（モジュラ逆数のような）オプションを解くことができるということです。Z3パワーモジュロステートメント

出典

2016-03-19 Owl Owl

Z3がその種の計算を特別にサポートしているかどうかを確認するだけですか？それとも解決策を求めていますか？満たされていないことを証明することに興味があれば、定量化された式としていくつかのpow-modルールをZ3に提供することができます。 – iago

私の質問の根拠は、それらの文を入力する良い方法があるのでしょうか？入力として、彼らは戻って非常に長い時間がかかります。残念ながら、私は実際に自分自身で問題を実際に助けるために数学の側（またはその問題のコーディング側）で十分にスマートではありません。答えのように聞こえるのは、今のところ、上記のやり方が正しいことだということです。 –

Z3はpow-modを特別にサポートしていないので、Z3を使ったpow-modに関連する問題を効率的に処理できないわけではありません。しかし、これはあなたの側でいくつかの前処理とエンコーディングトリックを必要とするかもしれません。具体的な問題の例を提示した場合、具体的なソリューション例について議論することもできます。 – iago

興味深い点。これは特にZ3ではサポートされていません。この分野で知られている技術は何ですか？

出典

2016-03-19 21:20:40

私は技術を理解していることは間違いありません。学部修学生の数年を経て、私はそのような問題のクラスを簡素化するためにその時にいくつかの技術を思い出しています。私が言うことから、Z3に直接記述されているpowmodは、解決のために非常に資源集中的です。 –

与えられた* x *と* y *を計算する順方向については、べき乗剰余算法は非常に効率的であり、通常、* x * mod * z *を二乗法* x^y * mod * z *を構築する* y *の分解。 * x *と* z *を指定した* y *を見つける逆の問題は、離散対数問題です。だから、Z3や他の誰にとっても難しいです。 –

Z3パワーモジュロステートメント

答えて

関連する問題