支持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)

• 它们不能决定可满足性的根本原因是什么？

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

Answer 1

是的，非线性整数运算对SMT求解器来说很困难有一个根本原因。Leo在https://stackoverflow.com/a/13898524/936310

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

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

开箱即用，你能做的最好的事情就是通过使c具体化来证明你的问题。即，添加表单的断言：

(assert (= c 12))

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