简化表达式会导致超时

Question

如何使用 Z3 Solver 简化以下表达式？

(declare-const c0 Int)
(declare-const c1 Int)
(declare-const c2 Int)

(assert (let ((a!1 (to_real (+ (* (* 2 c0) c2)
                   (* (* 2 c0) c1)
                   (* 2 c1 c2)
                   (* c0 (- c0 1))
                   (* c1 (- c1 1))))))
  (let ((a!2 (/ (to_real (* (* 2 c0) c2)) a!1)))
  (and (or (and (<= c2 1) (>= c2 1) (<= c0 2) (>= c0 2) (<= c1 3) (>= c1 3))
           (and (<= c2 1) (>= c2 1) (<= c0 3) (>= c0 3) (<= c1 2) (>= c1 2)))
  (= (/ 2.0 15.0) a!2))))
)

(apply (then qe propagate-values (repeat (then ctx-solver-simplify propagate-ineqs) 10)))

Link : http://rise4fun.com/Z3/u7F7

我尝试了所有我知道的可能策略，但最终导致求解器超时。有什么办法可以避免超时？是否假设 return false 导致 Java API?

Answer 1

仅通过查看该代码很难判断发生了什么。但我认为 to_real 可能是有问题的部分，因为域之间的转换往往会产生可能导致复杂性问题的非线性约束。

我会尝试使用纯实数（即，将 c0、c1.. 声明为 Reals；并删除对 to_real 的调用。 )

如果确实需要integers/reals混合；确保混合是在叶子上完成的（即，在常数）；或者在最高层，尽可能多地推动转换；而不是中间值。

但我想如果您的问题 space 允许的话，坚持使用 Reals 将是解决问题的方法。

Answer 2

该示例使用非线性整数运算。不幸的是，很容易在 Z3 不终止的域中生成示例。 ctx-solver-simplify 例程多次调用 SMT 求解器，并且在每次调用中都必须检查非线性约束的某些组合的可满足性。

简化表达式会导致超时

Simplifying an expression leads to time out

timeout

z3

simplify

java