cvc4中实数的对数/指数

Posted 2023-04-14

【中文标题】cvc4中实数的对数/指数

【英文标题】：Logarithm/Exponential of real numbers in cvc4

【发布时间】：2017-11-20 13:35:16

【问题描述】：

我正在寻找能够提供涉及对数或指数的实数公式模型的求解器。

cvc4 可以处理包含对数或实数指数的函数吗？ 同样，cvc4 可以表达常数e吗？

---

根据this question，z3 只能处理常数指数，这对我没有帮助。

This question 只询问整数的对数。

【参考方案1】：

我不熟悉 cvc4，但我可能有一些关于对数的有用属性，您可以根据自己的限制加以利用。

从技术上讲，没有计算机（无论多么强大）知道e 是什么，因为它是超越的（不能表示为具有有理系数的多项式方程的解）。

如果您受限于只能对整数取对数，则可以将e 表示为派系近似值并以这种方式求解。该公式最终比直接取对数要长一点，但优点是您可以有效地计算以任何有理数为底的对数，同时只能单独找到整数的对数。

让e 近似于分数a/b，其中a 和b 都是整数。

(a/b)^n = x

log(base a/b)(x) = n

这并不能真正带你去任何地方，所以我们必须走一条不同的路线，这需要更多的代数。

(a/b)^n = x

(a^n)/(b^n) = x

a^n = x * b^n

log(base a)(x * b^n) = n

log(base a)(x) + log(base a)(b^n) = n

log(base a)(x) + n*log(base a)(b) = n

log(base a)(x) = n - n*log(base a)(b)

log(base a)(x) = n * (1 - log(base a)(b))

n = log(base a)(x) / (1 - log(base a)(b))

换句话说，log(base a)(x) / (1 - log(base a)(b)) 是ln(x) 的近似值，其中a/b 是e 的近似值。显然，ln(x) 的这个近似值更接近ln(x) 的实际值，因为a/b 更接近于e。请注意，我在这里以一般形式保留了这一点，a/b 可以表示任何有理数，而不仅仅是e。

如果这不能完全回答您的问题，我希望它至少有所帮助。

---

随便试了一个例子。

如果您将a 和b 分别视为27183 和10000，我尝试了这个快速计算：

log(base 27183)(82834) / (1 - log(base 27138)(10000)) = 11.32452...

                                            ln(82834) = 11.32459...

【讨论】：

感谢您的回答！这可能是我的问题的解决方法。不过，我更喜欢不需要近似值的解决方案。这可能是可能的，例如在z3 中，sqrt(2) 也是可表达的。

@Peter 同样，e 是一个超越数。没有办法向计算机表达它可以准确地知道它是什么。 e 的近似值在处理计算机时是必需的。诸如sqrt(2) 之类的无理数可能会被计算机识别，因为尽管它不是重复小数，但它是方程x^2 - 2 = 0 的解。

感谢您的澄清！尽管如此，原则上还是可以解决涉及e 的一些 任务。例如，可以为exp(2)<x<exp(4)（可能使用e 的近似值）或2*e=x（只需输出x=e/2 对我有用）找到一个模型。但是如果z3 和cvc4 都不能处理这些，那么使用近似值似乎是下一个最佳解决方案。再次感谢您的指点！

@Peter 没问题。如果是这种情况，您能否（至少暂时，直到/如果其他人回答）将我的答案标记为已接受的答案？