如何将总和和乘积约束转换为 SMT-lib2（对于 Z3）

Question

我想知道将 sum 转换为 le 的最佳方法是什么

或类似的产品

转换为 SMT-lib2 表达式，专门用于使用 Z3（甚至是 metitarski）求解。

我认为使用量词会有一个明显的方法，但我在创建它时遇到了麻烦，并且在许多用例中，这样的总和可能有 exprLB 和 exprUB 的常量，这意味着我希望某种策略可以简单地将其展开为一长串加法，其中使用量词可能会使这变得更加困难。

例如，一个相当简单的转换策略

进入

这两者都被简单地表示为（并且被大多数 SMT 求解器简单地求解）为

(+ 
  (/ 2 x1)
  (/ 2 x2)
  (/ 2 x3)
)

yielding

sat (model (define-fun x1 () Real 1.0) (define-fun x2 () Real 1.0) (define-fun x3 () Real (/ 1.0 4.0)) )

如何在 smt-lib2 中优雅地表达三个表达式（下限、上限和累加器）的总和？

Answer 1

显而易见的选择是为您的 x 值使用数组，并使用递归函数对总和/积进行建模。

Z3 确实支持递归函数，但它不是万无一失的。充其量你会得到unknown,，因为大多数这样的公式都需要归纳证明； SMT求解器不擅长的事情。在最坏的情况下，您会得到一个无用的答案，或者如果您遇到错误，甚至可能会得到一个虚假的答案。

下面是一个成功的例子：

(declare-fun xs () (Array Int Real))
(define-fun-rec sum ((lb Int) (ub Int)) Real
   (ite (> lb ub)
        0
        (+ (select xs lb)
           (sum (+ lb 1) ub))))

(declare-fun lb () Int)
(declare-fun ub () Int)
(assert (= (sum lb ub) 12.34))
(check-sat)
(get-value (lb ub xs))

Z3 回应：

sat
((lb 0)
 (ub 0)
 (xs ((as const (Array Int Real)) (/ 617.0 50.0))))

这实际上很酷，虽然可能没有你想象的那么令人印象深刻。您也可以将其强制到某个范围：

(declare-fun xs () (Array Int Real))
(define-fun-rec sum ((lb Int) (ub Int)) Real
   (ite (> lb ub)
        0
    (+ (select xs lb)
       (sum (+ lb 1) ub))))

(declare-fun lb () Int)
(declare-fun ub () Int)
(assert (= 1 lb))
(assert (= 3 ub))
(assert (= (sum lb ub) 12.34))
(check-sat)
(get-value (lb ub))
(eval (select xs 1))
(eval (select xs 2))
(eval (select xs 3))

这会产生：

sat
((lb 1)
 (ub 3))
0.0
(- (/ 121233.0 50.0))
2437.0

这是一个正确的模型。不幸的是，对公式/断言的微小更改会导致它产生无用的答案。如果我尝试：

(declare-fun xs () (Array Int Real))
(define-fun-rec sum ((lb Int) (ub Int)) Real
   (ite (> lb ub)
        0
        (+ (/ 2.0 (select xs lb))
           (sum (+ lb 1) ub))))

(assert (= (sum 1 3) 12.34))
(check-sat)

然后我得到：

unknown

随着求解器对递归函数的支持越来越成熟，您当然可以期待它们能够成功回答更多查询。在短期内，您更有可能经常看到unknown 的回复。

就个人而言，我认为当您不知道总和/乘积中有多少项时使用 SMT 求解器并不是最好的主意。如果您知道术语的数量，请务必使用 SMT 求解器。如果没有，最好使用交互式定理证明，即允许您表达递归函数和归纳证明的系统；例如 Isabelle、Coq 等。