简化表达式会导致超时

Question

如何使用Z3求解器简化以下表达式?

(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)))

链接:http://rise4fun.com/Z3/u7F7

我尝试了我所知道的所有可能的策略，但最终还是导致求解器超时。有什么办法可以避免超时吗?是否应该返回false作为Java API的结果?

Answer 1

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

我会尝试使用纯粹的real(即声明c0, c1 ..)为Real s;并删除对to_real的调用。)

如果你需要整数/实数混合;确保混合是在叶子处完成的(即常数处);或者在最顶端，你可以尽可能地推动转换;而不是在中间值

但我想，如果你的问题空间允许的话，坚持使用real将是这里的方法。

Answer 2

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