1

考虑以下 SMTLIB 程序（在rise4fun此处）：

(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.arith.nl.gb false)

(declare-const n Int)
(declare-const i Int)
(declare-const r Int)

(assert (= i n))
(assert (= r (* i n)))

(push)
(assert (not (= r (* n n))))
(check-sat) ; unknown
(pop)

尽管它似乎只需要对句法相等进行推理，但 Z3（4.3.2 正式版，以及 4.4.0 b6c40c6c0eaf）仍然未能表明最终断言是unsat.

出乎意料（至少对我而言），设置smt.arith.nl.gb为true使示例验证（即check-sat产量unsat）。

对于它的价值，这里有一些进一步的观察：

  • 如果乘法分别更改为或，则可以显示最终断言unsat(* i n)(* n i)

  • 如果将乘法更改为，则无法显示unsat(* i i)

  • (push)并且(pop)似乎不会影响示例，即可以将它们删除而不影响所描述的观察结果

这是一个错误还是smt.arith.nl.gb需要显示此示例的原因unsat？

4

1 回答 1

2

这不一定是错误。基于 Groebner 的计算解决了这个问题，所以很快就找到了 unsat 结果（很好，所以默认启用）。此外，禁用 auto_config 还意味着根据问题未设置许多其他选项（但在这种特殊情况下没有区别）。

请注意，某些策略、求解器或简化器在看到乘法表达式时会简单地放弃，而不管问题是否恰好为人类或其他求解器容易解决。在这种特殊情况下，非线性求解器在 smt.arith.nl.rounds 用尽（默认为 1024）后放弃，因此它返回未知。

快速解决此问题的策略之一是 solve-eqs，但这不是默认策略的一部分（在这种情况下，它运行 qfnia 策略）。如果它解决了您的问题，您可以通过将 check-sat 命令替换为

(check-sat-using (then solve-eqs qfnia))

这是否应该是默认设置是值得商榷的并且可以进行基准测试，但这并不是一个真正的错误。

另一个快速解决这个问题的策略是 NLSAT 求解器，例如，

(check-sat-using nlsat)
于 2015-01-29T18:01:09.353 回答