哪些技术用于处理 z3 中的非线性整数实数问题？答案

【问题标题】：Which techniques are used to handle Non-linear Integer Real problems in z3?哪些技术用于处理 z3 中的非线性整数实数问题？
【发布时间】：2014-01-21 01:21:10
【问题描述】：

这是非线性整数实数片段中problem 的 z3 统计信息（我的许多问题都与此类似）：

 (:add-rows            11062574
  :added-eqs           34
  :arith-conflicts     37293
  :assert-lower        837747
  :assert-upper        1909779
  :binary-propagations 13807730
  :bound-prop          32666
  :conflicts           47631
  :decisions           157457
  :del-clause          32828
  :final-checks        39307
  :gcd-tests           329820
  :gomory-cuts         927
  :ineq-splits         19490
  :memory              39.52
  :minimized-lits      93912
  :mk-clause           73468
  :pivots              768193
  :propagations        15992318
  :pseudo-nonlinear    254856
  :restarts            41
  :time                151.65
  :total-time          151.68)

由于问题是非线性的，我相信 Simplex 技术并没有直接用于解决这个问题（尽管我在输出中看到了一些类似于 Simplex 的统计数据）。基于earlier 响应，我了解在存在整数的情况下的非线性实数技术基于 Grobner 基，并且相关函数在theory_arith* 中。是否有论文/一些文档，我可以在其中找到有关在 z3 中为此片段实现的技术的具体信息？

此外，尽管问题本身是非线性的，但唯一出现的非线性涉及两个变量的乘法（并且有一些这样的表达式），并且其中一个变量只能取幂的值两个并由一些简单的约束约束/定义：

(const1 <=  |a| < const2) => (var-a = const1)

其中 const1 和 const2 是 2 的连续正幂。因此，var-a 表示小于或等于 |a| 的 2 的最大幂。这些变量被声明为Real 类型。特别好奇，因为我在统计输出中看到了一个术语pseudo-nonlinear。约束是否以某种方式在内部被线性化？另外，是否有更好的方法来编码这些约束，以便 z3 在此类问题上做得更好？

【问题讨论】：

标签： z3 smt