smt.arith.nl.gb 对（句法）相等推理的意外影响 - 错误？

Question

考虑以下 SMTLIB 程序（在 rise4fun here 上）：

(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）。

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

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

无法显示

unsat

(push) 和 (pop) 似乎不影响示例，即它们可以在不影响描述的观察结果的情况下删除

这是错误还是需要 smt.arith.nl.gb 才能显示此示例 unsat？

Answer 1

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

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

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

来轻松添加它

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

这是否应该是默认值是有争议的，并且取决于基准测试，但这并不是真正的错误。

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

(check-sat-using nlsat)

smt.arith.nl.gb 对（句法）相等推理的意外影响 - 错误？

Unexpected effect of smt.arith.nl.gb on reasoning with (syntactic) equality - bug?

z3

equality

groebner-basis