使用 smt2 文件和 OCaml 在 Z3 中产生不同的结果

Question

我在 SMT2 和 OCaml 中遇到了同样的问题。使用 SMT2 文件，我可以在约 3 分钟内获得未饱和结果。然而，OCaml 中的同样问题被卡住了。请指教。

SMT2的问题：

(declare-fun x0 () (_ BitVec 32))
(declare-fun x1 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun y0 () (_ BitVec 32))
(declare-fun y1 () (_ BitVec 32))
(declare-fun y2 () (_ BitVec 32))

(assert (not (=> 
(and (= (bvadd x2 x1 x0) (bvadd y2 y1 y0))
     (= (bvadd x2 (bvmul #x00000002 x1) (bvmul #x00000003 x0)) 
        (bvadd y2 (bvmul #x00000002 y1) (bvmul #x00000003 y0)))
     (= (bvadd x2 (bvmul #x00000003 x1) (bvmul #x00000006 x0))
        (bvadd y2 (bvmul #x00000003 y1) (bvmul #x00000006 y0))))
     (= (bvadd x2 (bvmul #x00000004 x1) (bvmul #x0000000a x0))
        (bvadd y2 (bvmul #x00000004 y1) (bvmul #x0000000a y0))))))
(check-sat)

OCaml 中的同样问题：

let cfg = [("model", "true"); ("proof", "false")] in
let ctx = (mk_context cfg) in
let bv_sort = BitVector.mk_sort ctx 32 in
let c2 = Expr.mk_numeral_int ctx 2 bv_sort in
let c3 = Expr.mk_numeral_int ctx 3 bv_sort in
let c4 = Expr.mk_numeral_int ctx 4 bv_sort in
let c10 = Expr.mk_numeral_int ctx 10 bv_sort in
let c6 = Expr.mk_numeral_int ctx 6 bv_sort in
let x0 = Expr.mk_const ctx (Symbol.mk_string ctx "x0") bv_sort in
let x1 = Expr.mk_const ctx (Symbol.mk_string ctx "x1") bv_sort in
let x2 = Expr.mk_const ctx (Symbol.mk_string ctx "x2") bv_sort in
let y0 = Expr.mk_const ctx (Symbol.mk_string ctx "y0") bv_sort in
let y1 = Expr.mk_const ctx (Symbol.mk_string ctx "y1") bv_sort in
let y2 = Expr.mk_const ctx (Symbol.mk_string ctx "y2") bv_sort in
let ex1 = mk_add ctx (mk_add ctx x0 x1) x2 in
let ey1 = mk_add ctx (mk_add ctx y0 y1) y2 in
let ex2 = mk_add ctx (mk_add ctx (mk_mul ctx c3 x0) (mk_mul ctx x1 c2)) x2 in
let ey2 = mk_add ctx (mk_add ctx (mk_mul ctx c3 y0) (mk_mul ctx y1 c2)) y2 in
let ex3 = mk_add ctx (mk_add ctx (mk_mul ctx c6 x0) (mk_mul ctx x1 c3)) x2 in
let ey3 = mk_add ctx (mk_add ctx (mk_mul ctx c6 y0) (mk_mul ctx y1 c3)) y2 in
let ex4 = mk_add ctx (mk_add ctx (mk_mul ctx c10 x0) (mk_mul ctx x1 c4)) x2 in
let ey4 = mk_add ctx (mk_add ctx (mk_mul ctx c10 y0) (mk_mul ctx y1 c4)) y2 in
let left = Boolean.mk_and ctx [(mk_eq ctx ex1 ey1);(mk_eq ctx ex2 ey2);(mk_eq ctx ex3 ey3)] in
let right = mk_eq ctx ex4 ey4 in
let valid = Boolean.mk_implies ctx left right in
let sat = Boolean.mk_not ctx valid in

print_endline (Z3.Expr.to_string sat);
let solver = (mk_solver ctx None) in
Solver.add solver [sat];
let q = (check solver []) in
match q with
| SATISFIABLE -> print_endline "sat"
| UNSATISFIABLE -> print_endline "unsat"
| UNKNOWN -> print_endline "unknow";

Answer 1

这两个输入并不完全相同，因为其中一个输入具有相反顺序的所有加法器的参数，这会影响性能，因为 SAT 求解器中的启发式算法会进入不同的轨迹。我们可以通过改变参数的顺序然后使用 qfbv 策略来说服 OCaml API 表现出与 SMT2 版本相同的性能，如下所示：

let _ =
  let cfg = [("model", "true"); ("proof", "false")] in
  let ctx = (mk_context cfg) in
  let bv_sort = BitVector.mk_sort ctx 32 in
  let c2 = Expr.mk_numeral_int ctx 2 bv_sort in
  let c3 = Expr.mk_numeral_int ctx 3 bv_sort in
  let c4 = Expr.mk_numeral_int ctx 4 bv_sort in
  let c10 = Expr.mk_numeral_int ctx 10 bv_sort in
  let c6 = Expr.mk_numeral_int ctx 6 bv_sort in
  let x0 = Expr.mk_const ctx (Symbol.mk_string ctx "x0") bv_sort in
  let x1 = Expr.mk_const ctx (Symbol.mk_string ctx "x1") bv_sort in
  let x2 = Expr.mk_const ctx (Symbol.mk_string ctx "x2") bv_sort in
  let y0 = Expr.mk_const ctx (Symbol.mk_string ctx "y0") bv_sort in
  let y1 = Expr.mk_const ctx (Symbol.mk_string ctx "y1") bv_sort in
  let y2 = Expr.mk_const ctx (Symbol.mk_string ctx "y2") bv_sort in
  let ex1 = mk_add ctx x2 (mk_add ctx x1 x0) in
  let ey1 = mk_add ctx y2 (mk_add ctx y1 y0) in
  let ex2 = mk_add ctx x2 (mk_add ctx (mk_mul ctx x1 c2) (mk_mul ctx c3 x0)) in
  let ey2 = mk_add ctx y2 (mk_add ctx (mk_mul ctx y1 c2) (mk_mul ctx c3 y0) ) in
  let ex3 = mk_add ctx x2 (mk_add ctx (mk_mul ctx x1 c3) (mk_mul ctx c6 x0)) in
  let ey3 = mk_add ctx y2 (mk_add ctx (mk_mul ctx y1 c3) (mk_mul ctx c6 y0)) in
  let ex4 = mk_add ctx x2 (mk_add ctx (mk_mul ctx x1 c4) (mk_mul ctx c10 x0)) in
  let ey4 = mk_add ctx y2 (mk_add ctx (mk_mul ctx y1 c4) (mk_mul ctx c10 y0)) in
  let left = Boolean.mk_and ctx [(mk_eq ctx ex1 ey1);
                                 (mk_eq ctx ex2 ey2);
                                 (mk_eq ctx ex3 ey3)] in
  let right = mk_eq ctx ex4 ey4 in
  let valid = Boolean.mk_implies ctx left right in
  let sat = Boolean.mk_not ctx valid in  
  print_endline (Z3.Expr.to_string sat);
  let solver = (mk_solver_s ctx "QF_BV") in 
  (add solver [sat]) ;
  let q = (check solver []) in
  match q with
    | SATISFIABLE -> print_endline "sat"
    | UNSATISFIABLE -> print_endline "unsat"
    | UNKNOWN -> print_endline "unknown";

顺便说一句：请注意，为了解决名为“QF_BV”的逻辑的 SMT2 问题，Z3 将应用名为“qfbv”的策略。在这种特殊情况下，我们正在为逻辑“QF_BV”构造一个求解器，但如果我们想显式构造一个策略，那么

(mk_tactic ctx "QF_BV")

将因“无效参数”异常而失败。

以下关于性能差异的帖子可能会引起人们的兴趣：

What is the importance of the order of the assertions in Z3?

Z3 timing variation