编码返回“未知" [英] Encoding returns "unknown"

问题描述

对于这个例子:http://pastebin.com/QyebfD1p z3 和 cvc4 返回unknown"作为结果的检查周六.两者都不是很详细的原因，有没有办法让 z3 更详细地说明它的执行?

For this example: http://pastebin.com/QyebfD1p z3 and cvc4 return "unknown" as result of check-sat. Both are not very verbose about the cause, is there a way to make z3 more verbose about its execution ?

推荐答案

您的脚本使用了策略

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

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

This tactic applies the Z3 simplifier, and then executes a "general purpose" SMT solver available in Z3. This solver is not complete for nonlinear arithmetic. It is based on a combination of: Simplex, Interval Arithmetic and Grobner Basis. One of the big limitations of this module is that it can't find models/solutions containing irrational numbers. In the future, we will replace this module with new nonlinear solvers available in Z3.

对于非线性算术，我们通常建议使用 Z3 中可用的 nlsat 求解器.这是一个完整的过程，通常对于不可满足和可满足的实例非常有效.您可以在 这篇文章.要使用 nlsat，我们必须使用

For nonlinear arithmetic, we usually suggest the nlsat solver available in Z3. This is a complete procedure and is usually very effective for unsatisfiable and satisfiable instances. You can find more about nlsat in this article. To use nlsat, we have to use

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

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

Unfortunately, nlsat will get stuck in your example. It will get stuck computing Subresultants of very big polynomials produced during solving..

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

Z3 has yet another engine for handling nonlinear arithmetic. This engine reduces the problem to SAT. It is only effective on satisfiable problems that have solutions of the form a + b sqrt(2) where a and b are rational numbers. Using this engine, we can solve your problem in a very short amount of time. I attached the result in the end of the post. To use this engine, we have to use

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

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

EDIT Moreover, the tactic nla2bv encodes the rational numbers a and b as a pair of bit-vectors. By default, it uses bit-vectors of size 4. However, this value can be specified using the option nlsat_bv_size. This is not a global option, but an option provided to the tactic nla2bv. Thus, nla2bv can only find solutions of the form a + b sqrt(2) where a and b can be encoded using a small number of bits. If a satisfiable problem does not have a solution of this form, this tactic will fail and return unknown. END EDIT

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

Your example also suggests that we have to improve nlsat, and make it more effective as a model/solution finding procedure. The current version gets stuck when trying to show that the problem has no solution. We are aware of these limitations and are working on new procedures to workaround them.

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

BTW, in the Python front-end, Z3 displays the models/solutions in decimal notation. However, everything is computed precisely. To get the precise representation of the solution. We can use the method sexpr(). For example, I changed your loop to

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.

In the new loop, I'm displaying the result in decimal notation and the internal precise one. The meaning of (root-obj (+ (* 2 (^ x 2)) (* 12 x) (- 7)) 2) is the 2nd root of the polynomial 2*x^2 + 12x - 7.

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

EDIT Z3 provides combinators for creating non-trivial solvers. In the examples above, we used Then to perform the sequential composition of different tactics. We may also use OrElse to try different tactics. and TryFor(t, ms) that tries tactic t for ms milliseconds, and fails if the problem can't be solved in the given time. These combinators can be used to create tactics that use different strategies for solving a problem. END EDIT

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)

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

EDIT You can solve the problem in your comment by using the tactic

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

这个策略会在几秒钟内解决问题，并在帖子的最后给出解决方案.正如我上面所说，nlsat 是完整的，但可能需要很长时间.您的问题是当前版本的 Z3 可以自动决定/解决的问题的边缘.我们可以将不同的策略与OrElse 和TryFor 结合起来，使其更加稳定.示例:

This tactic will solve the problem in a couple of seconds, and produce the solution in the end of the post. As I said above, nlsat is complete, but it may take very long time. Your problem is on the fringe of what the current version of Z3 can decide/solve automatically. We can combine different tactics with OrElse and TryFor to make it more stable. Example:

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()

上面的策略尝试 nla2bv 方法 1 秒，然后 nlsat 1 秒，然后 nla2bv 10 秒，最后 nlsat 没有超时.

The tactic above tries the nla2bv approach for 1 sec, then nlsat for 1 sec, then nla2bv for 10 secs, and finally nlsat without a timeout.

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

I know this is not an ideal solution, but variations like that may be useful workarounds until the next solver for nonlinear arithmetic is ready. Moreover, Z3 has many other tactics that may be used to simplify/preprocess the problem before we invoke nlsat. END EDIT

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 中发生的事情.以下是一些可能性:

EDIT 2 Your problems are on the fringe of what Z3 can do in a reasonable amount of time. Nonlinear real arithmetic is decidable, but is very expensive. Regarding debugging/tracing what is going on in Z3. Here are some possibilities:

• 我们可以使用以下命令启用详细消息:set_option("verbose", 10).数字是详细级别:0 ==无消息"，更高的数字 ==更多消息".

• We can enable verbose messages using the command: set_option("verbose", 10). The number is the verbosity level: 0 == "no message", and higher numbers == "more messages".

编译支持跟踪的 Z3.有关详细信息，请参阅这篇文章.

Compile Z3 with support for tracing. See this post for more information.

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

Create a log of the Z3 APIs invoked by the Python program using the command open_log("z3.log"). This command should be invoked before any other Z3 API call. Then execute the log using the z3 executable inside of gdb. So, you will be able to stop the execution and find where Z3 is stuck. The nlsat solver usually gets stuck in two different places:

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

用代数系数隔离多项式的根(过程 isolate_roots 将在堆栈上).

isolating the roots of polynomials with algebraic coefficients (the procedure isolate_roots will be on the stack).

问题 2 将很快得到解决，在我们用 新的，效率更高.不幸的是，您的问题似乎卡在了子结果步骤中.

Problem 2 will be soon fixed, after we replace the old algebraic number package with the new one that is much more efficient. Unfortunately, it seems your problems get stuck in the subresultant step.

另一条评论:尽管 nla2bv 对您的原始基准测试有效，但您的新基准测试不太可能具有 a + b sqrt(2) 形式的解决方案，其中a 和 b 是有理数.因此，使用 nla2bv 只是开销.策略 nlsat 假设问题出在 CNF 中.所以，对于pastebin.com/QRCUQE10，我们必须先调用tseitin-cnf，然后再调用nlsat.另一种选择是使用大"策略qfnra-nlsat.在调用 nlsat 之前，它会调用许多预处理步骤.但是，其中一些步骤可能会使一些问题更难解决.

Another remarks: although nla2bv was effective for your original benchmark, it is unlikely your new benchmarks will have a solution of the form a + b sqrt(2) where a and b are rational numbers. So, using nla2bv is just overhead. The tactic nlsat assumes the problem to be in CNF. So, for pastebin.com/QRCUQE10, we have to invoke tseitin-cnf before invoking nlsat. Another option is to use "big" tactic qfnra-nlsat. It invokes many pre-processing steps before invoking nlsat. However, some of these steps may make some problems harder to solve.

结束编辑 2

这篇关于编码返回“未知"的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！