Z3 幂模语句答案

【问题标题】：Z3 Power Modulo StatementsZ3 幂模语句
【发布时间】：2016-03-19 20:48:17
【问题描述】：

Z3 有做幂模运算的能力吗？例如，如果我放置x ** y % z 类型的表达式，有没有办法告诉Z3 它是这种类型的表达式，类似于python 具有函数pow(x,y,z) 的方式？我的假设是这将打开求解选项（例如模逆）。

【问题讨论】：

你只是问Z3是否对这种算术有特殊支持？还是您在寻求解决方案？如果您有兴趣证明不可满足性，您可以为 Z3 提供一些 pow-mod 规则作为量化公式。
我想我的问题是有没有更好的方法来输入这些语句？作为输入，他们需要很长时间才能返回。不幸的是，我在数学方面（或编码方面）不够聪明，无法亲自帮助解决问题。听起来答案是，就目前而言，上面提到的方式是正确的方式，不管需要多长时间才能完成。
仅仅因为 Z3 没有对 pow-mod 的特定支持，并不意味着您不能有效地处理使用 Z3 涉及 pow-mod 的一些问题。但这可能需要您使用一些预处理和编码技巧。如果您提出一个具体的示例问题，也许我们可以讨论一个具体的示例解决方案。

【解决方案1】：

有趣的点。 Z3 对此没有任何特别的支持。该领域的已知技术有哪些？

【讨论】：

诚然，我对这些技术的理解已经脱离了我的元素。数学本科毕业已经很多年了，但我记得当时有一些技术可以简化这些问题。据我所知，直接在 Z3 中声明的 powmod 解决起来非常耗费资源。
对于给定 x 和 yx^y (mod z) /i>，模幂运算非常有效，通常通过反复平方 x mod z 来完成，使用 y 的二进制分解来构建x^y 模 z。但是，给定 x 和 z 求 y 的逆问题是离散对数问题，因此对于 Z3 或其他任何人来说都很难。跨度>