简化表达式会导致超时答案

【问题标题】：Simplifying an expression leads to time out简化表达式会导致超时
【发布时间】：2015-07-19 00:20:28
【问题描述】：

如何使用 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)))

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

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

【问题讨论】：

标签： timeout z3 simplify java

【解决方案1】：

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

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

如果您确实需要混合整数/实数；确保在叶子上进行混合（即，以常数）；或者在最顶端，尽可能多地推动转化；而不是中间值。

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

【讨论】：

【解决方案2】：

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

【讨论】：