0

我在以下 SMT 输入上执行了 z3 和 CVC4。两者都返回未知。

;!(a,b,c).(0<=a & 0<=b & 1<=c
;               =>
;               (a+(b mod c)) mod c = (a+b) mod c)
;
;
(set-logic NIA)
(set-option :print-success false)

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)

(assert (<= 0 a))
(assert (<= 1 c))
(assert (<= 0 b))

(assert (! (not (= (mod (+ a (mod b c)) c) (mod (+ a b) c))) :named goal))
(check-sat)
(exit)

  • 他们无法决定可满足性是否有任何根本原因？

  • 哪些选项或其他求解器适合解决此类问题？

4

1 回答 1

0

是的，非线性整数算术对于 SMT 求解器来说是困难的，这是有一个根本原因。Leo 在https://stackoverflow.com/a/13898524/936310中彻底解释了这一点

因此，期望 SMT 求解器在该领域表现出色是不合理的。建议使用适当的定理证明器，如 Isabelle、Coq、Lean、ACL2、HOL、HOL-Light 等。当然，证明大多是手动的，但这些系统通常与 SMT 求解器连接以实现许多目标，就可判定性而言，为您提供两全其美的体验。

请注意，即使(check-sat-using qfnra-nlsat)Leo 描述的技巧也不适用于您的问题，因为对modover real 的解释根本不会帮助您。（一般来说，这个qfnra-nlsat技巧可以找到模型，但永远不会产生unsat，因为它主要是一种模型搜索策略。）

您可以开箱即用的最好方法是通过制作c具体来证明您的问题的实例。即，添加以下形式的断言：

(assert (= c 12))

你会看到 z3 立即返回unsat。当然，这还不够，但您暂时无法使用按钮求解器做得更好（除非他们为这个问题添加“自定义”启发式方法！）。

于 2020-07-27T14:07:42.933 回答