哪些技术用于处理 z3 中的非线性整数实数问题? [英] Which techniques are used to handle Non-linear Integer Real problems in z3?

问题描述

以下是针对 问题 的 z3 统计数据Linear Integer Real Fragment(我的很多问题都与此类似):

Here are z3 statistics for a problem in the Non-Linear Integer Real Fragment (and many of my problems are similar to this):

 (: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 的统计数据).根据之前的回复，我了解了Integers 的存在基于 Grobner 基，相关函数在 theory_arith* 中.是否有论文/一些文档可以找到有关在 z3 中为此片段实现的技术的特定信息?

Since the problem is non-linear, I believe the Simplex technique is not directly being used to solve this (although I see some Simplex-like statistics in the output). Based on an earlier response, I understand the non-linear Real technique in the presence of Integers is based on Grobner bases, and that the relevant functions are in theory_arith*. Is there a paper/some documentation where I could find specific information about the techniques that are implemented in z3 for this fragment?

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

Also, although the problem is non-linear as such, the only occurrence of non-linearity involve multiplication of two variables (and there are a few such expressions), and one of the variables can only taken on values that are powers of two and bound/defined by some simple constraints:

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

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

where const1 and const2 are consecutive positive powers of two. Thus, var-a represents the largest power of two lesser than or equal to |a|. These variables were declared to be of type Real. Especially curious since I see a term pseudo-nonlinear in the stats output. Are the constraints being linearized internally, in some way? Also, is there a better way to encode these constraints so that z3 does better on such problems?

推荐答案

查看以下相关问题:

• Z3 如何处理非线性整数算术?

以下内容也可能相关:

• 需要帮助理解等式

结合非线性实数和线性整数

Z3 支持非线性算术

z3 在处理非线性实数算术方面的限制

这篇关于哪些技术用于处理 z3 中的非线性整数实数问题?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！