SMT求解器中整数除法的支持

Question

我已经对下面的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)

为什么他们不能决定satisfiability?，

• 有什么根本原因吗？

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

Answer 1

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

因此，期望SMT求解者在这一领域做得很好是完全不合理的。建议是使用适当的定理证明，如伊莎贝尔，Coq，精益，ACL2，HOL，HOL等。当然，这些证明大多是手动的，但这些系统通常与SMT求解器有连接，以实现许多目标，就可判定性而言，这两个世界都是最好的。

请注意，即使是Leo描述的(check-sat-using qfnra-nlsat)技巧也不能解决您的问题，因为对real的mod的解释在这里根本帮不了您。(一般来说，qfnra-nlsat技巧可以找到模型，但不会产生unsat，因为它主要是一种模型搜索策略。)

你能做的最好的事情就是通过c混凝土来证明你的问题的实例。即增加一种形式的断言：

(assert (= c 12))

您将看到z3立即返回unsat。当然，这还不够，但是使用按钮求解器不能做得更好(除非他们为这个问题添加了“自定义”启发式！)暂时。