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.gbtrue使示例验证(即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 回答