在给定的时间限制之后,Z3中的TryFor不会停止检查

Question

我使用的是Z3的.NET API.当我通过调用实例化解算器时:

Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit));

对于某些型号的声明,给它一个60秒(60000毫秒)的TimeLimit

s.Check()

60秒后不返回.对于某些型号,它会在几秒钟后返回,在我的情况下不会出现问题,但对于某些型号它根本不会返回(我在3天后取消了该过程).

如何在给定的时间限制后强制Z3停止检查？

Answer 1

组合TryFor器是使用“取消”标志来实现的。新策略反应非常灵敏，并且在设置“取消”标志时很快终止。不幸的是，通用策略smt是通用求解器的包装。这个通用求解器的响应速度不是很快。它可能会在几个关键地方“迷失”：量词实例化、单纯形等。该qflia策略建立在 和许多其他策略之上smt。因为，您正在尝试解决无量词的问题。我假设该smt策略位于 Simplex 模块内部的循环中。该smt策略中的 Simplex 模块是使用任意精度有理数实现的。因此，对于非平凡的线性实/整数问题可能非常耗时。

您无能为力解决此问题。如果你确实需要运行时间的强有力保证，我看到的唯一解决方案是创建一个单独的进程运行Z3，并在k解决问题需要更多秒数时杀死它。

话虽如此，Z3的未来版本将拥有全新的算术模块。当设置取消标志时，这个新模块（就像新策略一样）将快速终止。