1

对于此示例：http : //pastebin.com/QyebfD1p z3 和 cvc4 作为 check-sat 的结果返回“未知”。两者都不是很详细的原因，有没有办法让 z3 对其执行更详细？

4

1 回答 1

2

您的脚本使用该策略

s = Then('simplify','smt').solver()

此策略应用 Z3 简化器，然后执行 Z3 中可用的“通用”SMT 求解器。这个求解器对于非线性算术来说是不完整的。它基于以下组合：单纯形法、区间算术法和格罗布纳基法。该模块的一大限制是它无法找到包含无理数的模型/解决方案。将来，我们将用 Z3 中可用的新非线性求解器替换此模块。

对于非线性算术，我们通常建议在 Z3 中使用 nlsat 求解器。这是一个完整的过程，通常对于不可满足和可满足的情况非常有效。您可以在本文中找到有关 nlsat 的更多信息。要使用 nlsat，我们必须使用

s = Tactic('qfnra-nlsat').solver()

不幸的是， nlsat 会卡在您的示例中。计算求解过程中产生的非常大多项式的子结果时会卡住..

Z3 还有另一个处理非线性算术的引擎。该引擎将问题减少到 SAT。它只对有理数形式a + b sqrt(2)的解a的可满足问题有效。b使用这个引擎，我们可以在很短的时间内解决您的问题。我在帖子末尾附上了结果。要使用这个引擎，我们必须使用

s = Then('simplify', 'nla2bv', 'smt').solver()

编辑此外，该策略nla2bv将有理数编码a为b一对位向量。默认情况下，它使用大小为 4 的位向量。但是，可以使用选项指定此值nlsat_bv_size。这不是全局选项，而是提供给 tactic 的选项nla2bv。因此，nla2bv只能找到形式的解决方案，a + b sqrt(2)可以a使用b少量比特进行编码。如果一个可满足的问题没有这种形式的解决方案，这个策略就会失败并返回unknown。 结束编辑

您的示例还表明我们必须改进 nlsat，并使其作为模型/解决方案查找程序更有效。当前版本在试图表明问题没有解决方案时会卡住。我们知道这些限制，并正在制定新的程序来解决这些限制。

顺便说一句，在 Python 前端，Z3 以十进制表示法显示模型/解决方案。然而，一切都是精确计算的。以获得解决方案的精确表示。我们可以使用方法sexpr()。例如，我将您的循环更改为

for d in m.decls():
    print "%s = %s = %s" % (d.name(), m[d], m[d].sexpr())

在新循环中，我以十进制表示法和内部精确表示法显示结果。的含义(root-obj (+ (* 2 (^ x 2)) (* 12 x) (- 7)) 2)是多项式的二次根2*x^2 + 12x - 7。

EDIT Z3 提供了用于创建非平凡求解器的组合器。在上面的例子中，我们习惯于Then执行不同策略的顺序组合。我们也可能会OrElse尝试不同的战术。并且TryFor(t, ms)会尝试几毫秒的策略t，ms如果在给定时间内无法解决问题，则会失败。这些组合器可用于创建使用不同策略来解决问题的策略。 结束编辑

sat
Presenting results
traversing model...
s_2_p_p = 0.5355339059? = (root-obj (+ (* 2 (^ x 2)) (* 12 x) (- 7)) 2)
s_1_p_p = 0 = 0.0
s_init_p_p = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
s_2_p = 0.7071067811? = (root-obj (+ (* 2 (^ x 2)) (- 1)) 2)
s_1_p = 0 = 0.0
s_init_p = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
epsilon = 0 = 0.0
p_b2_s2_s_sink = 0.9142135623? = (root-obj (+ (* 4 (^ x 2)) (* 4 x) (- 7)) 2)
p_b2_s2_s_target = 0.0857864376? = (root-obj (+ (* 4 (^ x 2)) (* (- 12) x) 1) 1)
p_b2_s2_s_2 = 0 = 0.0
p_b2_s2_s_1 = 0 = 0.0
p_a2_s2_s_sink = 0 = 0.0
p_a2_s2_s_target = 0.8284271247? = (root-obj (+ (^ x 2) (* 4 x) (- 4)) 2)
p_a2_s2_s_2 = 0.1715728752? = (root-obj (+ (^ x 2) (* (- 6) x) 1) 1)
p_a2_s2_s_1 = 0 = 0.0
sigma_s2_b2 = 1 = 1.0
sigma_s2_a2 = 0 = 0.0
p_b1_s1_s_sink = 1 = 1.0
p_b1_s1_s_target = 0 = 0.0
p_b1_s1_s_2 = 0 = 0.0
p_b1_s1_s_1 = 0 = 0.0
p_a1_s1_s_sink = 1 = 1.0
p_a1_s1_s_target = 0 = 0.0
p_a1_s1_s_2 = 0 = 0.0
p_a1_s1_s_1 = 0 = 0.0
sigma_s1_b1 = 0 = 0.0
sigma_s1_a1 = 1 = 1.0
p_sinit_sink = 0.7071067811? = (root-obj (+ (* 2 (^ x 2)) (- 1)) 2)
p_sinit_target = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)
p_sinit_2 = 0 = 0.0
p_sinit_1 = 0 = 0.0
s_sink = 0 = 0.0
s_target = 1 = 1.0
s_2 = 0.0857864376? = (root-obj (+ (* 4 (^ x 2)) (* (- 12) x) 1) 1)
s_1 = 0 = 0.0
s_init = 0.2928932188? = (root-obj (+ (* 2 (^ x 2)) (* (- 4) x) 1) 1)

编辑 您可以使用该策略解决评论中的问题

s = Then('simplify', 'nlsat').solver()

这种策略将在几秒钟内解决问题，并在帖子末尾产生解决方案。正如我上面所说，nlsat是完整的，但可能需要很长时间。您的问题处于 Z3 的当前版本可以自动决定/解决的边缘。我们可以将不同的策略与OrElseand结合起来TryFor，使其更加稳定。例子：

s = OrElse(TryFor(Then('simplify', 'nla2bv', 'smt', 'fail-if-undecided'), 1000),
           TryFor(Then('simplify', 'nlsat'), 1000),
           TryFor(Then('simplify', 'nla2bv', 'smt', 'fail-if-undecided'), 10000),
           Then('simplify', 'nlsat')).solver()

上面的策略尝试了nla2bv1 秒，然后nlsat是 1 秒，然后nla2bv是 10 秒，最后nlsat没有超时。

我知道这不是一个理想的解决方案，但在下一个非线性算术求解器准备好之前，这样的变体可能是有用的解决方法。此外，Z3 还有许多其他策略可用于在我们调用之前简化/预处理问题nlsat。 结束编辑

s_init = 15/32
s_1 = 7/16
s_2 = 1/2
s_target = 1
s_sink = 0
p_sinit_1 = 1/2
p_sinit_2 = 1/4
p_sinit_target = 1/8
p_sinit_sink = 1/8
sigma_s1_a1 = 1/2
sigma_s1_b1 = 1/2
p_a1_s1_s_1 = 1/2
p_a1_s1_s_2 = 1/4
p_a1_s1_s_target = 1/8
p_a1_s1_s_sink = 1/8
p_b1_s1_s_1 = 1/2
p_b1_s1_s_2 = 1/4
p_b1_s1_s_target = 1/16
p_b1_s1_s_sink = 3/16
sigma_s2_a2 = 1/2
sigma_s2_b2 = 1/2
p_a2_s2_s_1 = 1/2
p_a2_s2_s_2 = 1/4
p_a2_s2_s_target = 11/64
p_a2_s2_s_sink = 5/64
p_b2_s2_s_1 = 3/4
p_b2_s2_s_2 = 1/32
p_b2_s2_s_target = 9/64
p_b2_s2_s_sink = 5/64
epsilon = 1/4
s_init_p = 1649/3520
s_1_p = 797/1760
s_2_p = 103/220
s_init_p_p = 1809/3904
s_1_p_p = 813/1952
s_2_p_p = 127/244

编辑 2 您的问题处于 Z3 在合理时间内可以做的事情的边缘。非线性实数算术是可判定的，但是非常昂贵。关于调试/跟踪 Z3 中发生的事情。以下是一些可能性：

  • 我们可以使用以下命令启用详细消息：set_option("verbose", 10). 数字是详细程度：0 ==“无消息”，更高的数字==“更多消息”。

  • 编译支持跟踪的 Z3。有关更多信息，请参阅此帖子。

  • 使用命令创建 Python 程序调用的 Z3 API 的日志open_log("z3.log")。此命令应在任何其他 Z3 API 调用之前调用。然后z3使用gdb. 因此，您将能够停止执行并找到 Z3 卡住的位置。nlsat求解器通常会卡在两个不同的地方：

    1. 计算子结果（过程psc_chain将在堆栈上），以及

    2. 用代数系数隔离多项式的根（该过程isolate_roots将在堆栈上）。

在我们用效率更高的新代数包替换旧代数包之后，问题 2 将很快得到解决。不幸的是，您的问题似乎停留在子步骤中。

另一个评论：虽然nla2bv对您的原始基准有效，但您的新基准不太可能有形式的解，a + b sqrt(2)其中a和b是有理数。所以，使用nla2bv只是开销。该策略nlsat假定问题出在 CNF 中。因此，对于pastebin.com/QRCUQE10，我们必须在调用tseitin-cnf之前调用nlsat。另一种选择是使用“大”策略qfnra-nlsat。它在调用之前调用了许多预处理步骤nlsat。但是，其中一些步骤可能会使一些问题更难解决。

结束编辑 2

于 2013-02-11T23:32:22.753 回答