在 OCaml 中使用 Z3 获得无界变量的解释

Question

问题

我尝试使用 Z3 优化功能在检查可满足性时考虑一些目标。当我要求 Z3 使用

x + y

和

x > 0

最小化

y > 0

时，使用 get_model 获得的解释将

1

分配给

x

和

y

。然而，我有兴趣获得“更接近”最佳解决方案的解释。我尝试了一种解决方法（我将在下面解释），但我想知道 Z3 中是否存在一些“内置”功能，可以“更好”地解释无限目标。

我尝试了什么

我尝试使用 get_lower 和 get_upper，它们为

x + y

赋予了符号值——即

2 * epsilon

。然后，我使用 substitute_one 将

epsilon

替换为一些“非常小的”选择值（例如：

0.001

）。我可以将获得的

x + y

值（这是我试图最小化的表达式）注入到求解器中。一个 get_model 就足够了。

这是我尝试的示例，查看不同 Z3 函数的结果：

open Z3
open Z3.Expr
open Z3.Boolean
open Z3.Arithmetic
open Z3.Arithmetic.Real
open Z3.Optimize
open Z3.Solver
open Z3.Model
open Printf

let ctx = Z3.mk_context [] (* context object *)
let opt = Optimize.mk_opt ctx (* optimization context *)

let x = Real.mk_const_s ctx "x"
let y = Real.mk_const_s ctx "y"
let zero = Real.mk_numeral_i ctx 0
let x_plus_y = Real.mk_const_s ctx "x_plus_y"

let assertions = 
  Arithmetic.mk_gt ctx x zero (* x > 0 *)
  :: Arithmetic.mk_gt ctx y zero (* y > 0 *)
  :: Boolean.mk_eq ctx x_plus_y (Arithmetic.mk_add ctx [x; y]) (* x_plus_y = x + y *)
  :: []

(* assert constraints into the optimize solver *)
let () = Optimize.add opt assertions

(* ask the solver to minimize x_plus_y *)
let handle = Optimize.minimize opt x_plus_y

(* check sat *)
let status = Optimize.check opt

let () = Z3.Params.set_print_mode ctx PRINT_SMTLIB_FULL
let () = printf "- status: %s\n\n" @@ Solver.string_of_status status

(* get a model when SAT *)
let () = if status == SATISFIABLE then
  match Optimize.get_model opt with
  | None -> ()
  | Some model -> 
    printf "- model:\n%s\n" @@ Model.to_string model;
    printf "- objectives:";
    List.iter 
      (fun expr -> printf " %s\n" @@ Expr.to_string expr) 
      @@ Optimize.get_objectives opt;
    printf "- lower_bound: %s\n" 
      @@ Expr.to_string 
      @@ Optimize.get_lower handle;
    printf "- upper_bound: %s\n\n" 
      @@ Expr.to_string 
      @@ Optimize.get_upper handle;
    printf "- substitute epsilon with 0.001: %s\n\n" 
      @@ Expr.to_string
      @@ Expr.substitute_one
           (Optimize.get_lower handle)
           (Real.mk_const_s ctx "epsilon")
           (Real.mk_numeral_s ctx @@ string_of_float 0.001);

给出以下输出：

- status: satisfiable

- model:
y -> 1.0
x -> 1.0
x_plus_y -> 2.0

- objectives: x_plus_y
- lower_bound: (* 2.0 epsilon)
- upper_bound: (* 2.0 epsilon)

- substitute epsilon with 0.001: (* 2.0 (/ 1.0 1000.0))

问题

• 我不确定get_lower和get_upper的用途。在我的示例中，它们返回完全相同的值。是否有任何资源解释在此上下文中下限和上限的含义？
• 有没有其他方法来评估目标（除了像我一样替换

  epsilon

  ）？

谢谢。

Answer 1

一般来说，如果目标本身不是具体（即有限）值，则不能依赖模型中找到的值。确保安全的一种方法是确保将变量添加到优化目标中。 （即，每个变量都成为一个目标。）您可以使用字典顺序将它们推到您尝试优化的实际目标之后，这样就不会干扰实际的优化过程。

假设您执行上述操作（即您的每个变量也是一个优化目标），那么您只需查看目标。 （即，根本不看模型。）并从那里收集值。如果你的变量有无限的值，那么你能说的几乎就这些了。据我所知，没有任何方法可以进一步推断出任何内容。

我不一定依赖

get_lower

/

get_higher

。这些充其量只是“暗示性的”。即，不能保证它们以精确的方式为您提供可满足性区间。 （您可以将它们视为“当前近似值”，但解算器的其他部分可以介入使它们变得无关紧要。）

在实践中，我想说如果你正在优化，只使用客观值。并添加足够的约束以确保您的目标始终是有限的。特别是，z3 不支持严格不等式的优化。 （例如参见https://github.com/Z3Prover/z3/issues/3595）。因此，当涉及到这些时，我不一定会指望结果，这并不明显。 （除非你真的确定你的约束是什么。这在库代码或更复杂的场景中可能并不容易/不可能。）