1

我在 Z3 中有以下模型（将代码粘贴到http://research.microsoft.com/en-us/um/redmond/projects/z3/以进行尝试）。Web 界面给了我一个解决方案，见下文。但是，当我通过 .NET 求解同一模型并使用 Evaluate() 获取变量值时，我得到了不同的输出，我不明白。如您所见，我得到的不是值，而是表达式。我的问题是：如何获取 .NET 中的值？作为记录，我仔细检查了我在 .NET 中构建的模型是否与此处粘贴的模型相同。我还看到了这篇文章：发布并尝试应用修复（将 auto_config 设置为 false），但这只会导致求解器无法计算解决方案。

模型：

    Q311, Q411, Q431, QQ311, QQ411, QQ431, H11, H41 = Reals('Q311 Q411 Q431 QQ311 QQ411 QQ431 H11 H41')
solve(
Q411 + Q311 <= 155,
Q431 - Q311 <= -28.015,
-Q431 - Q411 <= -126.985,
-Q411 - Q311 <= -155,
-Q431 + Q311 <= 28.015,
Q431 + Q411 <= 126.985,
43.015 - H11 - 0.0031 * QQ311 * Q311 <= 0,
H41 - H11 - 0.0031 * QQ411 * Q411 <= 0,
H41 - 43.015 - 0.0031 * QQ431 * Q431 <= 0,
-43.015 + H11 + 0.0031 * QQ311 * Q311 <= 0,
-H41 + H11 + 0.0031 * QQ411 * Q411 <= 0,
-H41 + 43.015 + 0.0031 * QQ431 * Q431 <= 0,
QQ311 - Q311 <= 0,
QQ411 - Q411 <= 0,
QQ431 - Q431 <= 0,
-QQ311 + Q311 <= 0,
-QQ411 + Q411 <= 0,
-QQ431 + Q431 <= 0,
Q311 >= 0,
Q411 >= 0,
Q431 >= 0,
QQ311 >= 0,
QQ411 >= 0,
QQ431 >= 0,
H11 >= 0,
H41 >= 0,
show=True)

网页界面解决方案：

[Q411 = 83.5779688745?,
Q311 = 71.4220311254?,
Q431 = 43.4070311254?,
H11 = 27.2015697567?,
QQ311 = 71.4220311254?,
H41 = 48.8559280884?,
QQ411 = 83.5779688745?,
QQ431 = 43.4070311254?]

.NET 解决方案：

Q311: (root-obj (+ (* 40000 (^ x 2)) (* 10158800 x) (- 929606391)) 2)
Q411: (root-obj (+ (* 40000 (^ x 2)) (* (- 22558800) x) 1606007609) 1)
Q431: (root-obj (+ (* 20 (^ x 2)) (* 6200 x) (- 306807)) 2)
QQ431: (root-obj (+ (* 20 (^ x 2)) (* 6200 x) (- 306807)) 2)
H11: (root-obj (+ (* 160000000000000000 (^ x 2)) (* 41281815903200000000 x) (- 1
241318258533436869359)) 2)
QQ311: (root-obj (+ (* 40000 (^ x 2)) (* 10158800 x) (- 929606391)) 2)
H41: (root-obj (+ (* 40000000000 (^ x 2)) (* (- 19162006800000) x) 8407015578762
89) 1)
QQ411: (root-obj (+ (* 40000 (^ x 2)) (* (- 22558800) x) 1606007609) 1)
4

1 回答 1

1

阅读这篇文章后，我能够理解输出。

我将 { "PP_DECIMAL", "true"} 添加到我的上下文配置中，现在我得到了我预期的十进制值。

于 2012-08-05T12:42:12.857 回答