z3 - 战术求解器超时的不正确行为

Question

我正在尝试在 Z3 中使用策略求解器来解决一些 X 约束的问题，而不是通用求解器。

我正在使用以下策略 -

simplify purify-arith elim-term-ite reduce-args propagate-values solve-eqs symmetry-reduce smt sat sat-preprocess

我通过使用Z3_tactic_and_thenAPI 将策略一个接一个地应用到问题上。我也在使用这种技术来配置求解器的超时。

现在，对于同样的问题，如果我使用通用求解器，它会在指定超时的查询中超时。但是，如果我对求解器使用上述策略，那么它不会在给定时间内超时。它运行的时间更长。

例如，我指定了超时180*1000 milliseconds，但它在 730900 毫秒后超时。我试图删除上面提到的一些策略，但行为仍然相同。

Z3 版本 4.1

Answer 1

不幸的是，并非每种策略都尊重超时。该战术smt是一个大“罪犯”。这个策略包含了一个在 Z3 中实现的非常古老的求解器。不幸的是，这个求解器在一些昂贵的计算过程中不能被中断，因为它会使系统处于损坏状态。也就是说，Z3 在以后的操作中会崩溃。实施此求解器时，使用了非常简单的设计。如果我们想中断进程：kill it。当然，在更大的应用程序中使用 Z3 时，这是不可接受的。新代码通常对超时响应更快，我们尽量避免这种糟糕的设计。