我在 UFBV 查询上运行 Z3。目前该查询包含 2 个调用check-sat。如果我紧跟push 1在 之后check-sat，Z3 会在 30 秒内解决查询。如果我根本不放任何东西push 1，因此有两个电话之间check-sat没有任何电话push 1，那么 Z3 会在 200 秒内解决它。有趣的。有什么具体原因还是只是巧合？
问问题
1103 次
1 回答
7
Z3 3.x 有一个基于战术和战术的“战略规范语言”。我还没有“做广告”，因为它正在进行中。此幻灯片中描述了基本思想。我们对每个逻辑都有不同的内置策略。这些策略通常不支持增量求解，因为它们可能会应用使用“封闭世界”假设的转换。例如，我们有将 0-1 线性整数算术映射到 SAT 的转换。每当 Z3 检测到用户“想要”增量求解（例如，多个check-sat命令push和pop命令）时，它就会切换到通用求解器。在未来的版本中，我们将提供更多用于控制 Z3 行为的功能。
BTW，如果你有两个连续的(check-sat) (check-sat)命令，Z3 不一定进入增量模式。只有在两个调用之间有assertor命令时才会进入。push
现在，假设您的查询格式为：(check-sat) <assertions> (check-sat)，而您的第二个查询格式为(check-sat) <assertions> (push) (check-sat)。在这两种情况下，Z3 将在第二个中处于增量模式(check-sat)。但是，行为仍然不一样。增量求解器将断言的公式“编译”为内部格式，如果push执行了命令，则会影响其行为。例如，仅当没有用户范围时，它才会使用更有效的二进制子句编码。通过用户范围，我的意思是push命令的数量 - 命令的数量pop。这样做是因为在更有效的编码中使用的数据结构没有有效的撤消/逆操作。
于 2012-02-03T17:06:34.177 回答